Welcome to Abella 2.0.4-dev

Abella < Specification "stlc-strong-norm".
Reading specification "stlc-strong-norm"

Abella < Close tm, ty.

Abella < Define sn : tm -> prop by 
sn M := forall N, {step M N} -> sn N.

Abella < Define neutral : tm -> prop by 
neutral M := forall A R, M = abs A R -> false.

Abella < Define reduce : tm -> ty -> prop by 
reduce M top := {of M top} /\ sn M;
reduce M (arrow A B) := {of M (arrow A B)} /\ (forall U, reduce U A -> reduce (app M U) B).
Warning: Definition might not be stratified
 ("reduce" occurs to the left of ->)

Abella < Theorem reduce_of : 
forall A M, reduce M A -> {of M A}.

============================
 forall A M, reduce M A -> {of M A}

reduce_of < intros.

Variables: A M
H1 : reduce M A
============================
 {of M A}

reduce_of < case H1.

Subgoal 1:

Variables: M
H2 : {of M top}
H3 : sn M
============================
 {of M top}

Subgoal 2 is:
 {of M (arrow A1 B)}

reduce_of < search.

Subgoal 2:

Variables: M B A1
H2 : {of M (arrow A1 B)}
H3 : forall U, reduce U A1 -> reduce (app M U) B
============================
 {of M (arrow A1 B)}

reduce_of < search.
Proof completed.

Abella < Define ctx : olist -> prop by 
ctx nil;
nabla x, ctx (of x A :: L) := {ty A} /\ ctx L.

Abella < Define name : tm -> prop by 
nabla x, name x.

Abella < Theorem ctx_member : 
forall E L, ctx L -> member E L ->
  (exists X A, E = of X A /\ name X /\ {ty A}).

============================
 forall E L, ctx L -> member E L ->
   (exists X A, E = of X A /\ name X /\ {ty A})

ctx_member < induction on 1.

IH : forall E L, ctx L * -> member E L ->
       (exists X A, E = of X A /\ name X /\ {ty A})
============================
 forall E L, ctx L @ -> member E L ->
   (exists X A, E = of X A /\ name X /\ {ty A})

ctx_member < intros.

Variables: E L
IH : forall E L, ctx L * -> member E L ->
       (exists X A, E = of X A /\ name X /\ {ty A})
H1 : ctx L @
H2 : member E L
============================
 exists X A, E = of X A /\ name X /\ {ty A}

ctx_member < case H1.

Subgoal 1:

Variables: E
IH : forall E L, ctx L * -> member E L ->
       (exists X A, E = of X A /\ name X /\ {ty A})
H2 : member E nil
============================
 exists X A, E = of X A /\ name X /\ {ty A}

Subgoal 2 is:
 exists X A, E n1 = of X A /\ name X /\ {ty A}

ctx_member < case H2.

Subgoal 2:

Variables: E L1 A
IH : forall E L, ctx L * -> member E L ->
       (exists X A, E = of X A /\ name X /\ {ty A})
H2 : member (E n1) (of n1 A :: L1)
H3 : {ty A}
H4 : ctx L1 *
============================
 exists X A, E n1 = of X A /\ name X /\ {ty A}

ctx_member < case H2.

Subgoal 2.1:

Variables: L1 A
IH : forall E L, ctx L * -> member E L ->
       (exists X A, E = of X A /\ name X /\ {ty A})
H3 : {ty A}
H4 : ctx L1 *
============================
 exists X A1, of n1 A = of X A1 /\ name X /\ {ty A1}

Subgoal 2.2 is:
 exists X A, E n1 = of X A /\ name X /\ {ty A}

ctx_member < search.

Subgoal 2.2:

Variables: E L1 A
IH : forall E L, ctx L * -> member E L ->
       (exists X A, E = of X A /\ name X /\ {ty A})
H3 : {ty A}
H4 : ctx L1 *
H5 : member (E n1) L1
============================
 exists X A, E n1 = of X A /\ name X /\ {ty A}

ctx_member < apply IH to H4 H5.

Subgoal 2.2:

Variables: L1 A X A1
IH : forall E L, ctx L * -> member E L ->
       (exists X A, E = of X A /\ name X /\ {ty A})
H3 : {ty A}
H4 : ctx L1 *
H5 : member (of (X n1) A1) L1
H6 : name (X n1)
H7 : {ty A1}
============================
 exists X1 A, of (X n1) A1 = of X1 A /\ name X1 /\ {ty A}

ctx_member < search.
Proof completed.

Abella < Theorem ty_ignores_ctx : 
forall L A, ctx L -> {L |- ty A} -> {ty A}.

============================
 forall L A, ctx L -> {L |- ty A} -> {ty A}

ty_ignores_ctx < induction on 2.

IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
============================
 forall L A, ctx L -> {L |- ty A}@ -> {ty A}

ty_ignores_ctx < intros.

Variables: L A
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H2 : {L |- ty A}@
============================
 {ty A}

ty_ignores_ctx < case H2.

Subgoal 1:

Variables: L
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
============================
 {ty top}

Subgoal 2 is:
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

ty_ignores_ctx < search.

Subgoal 2:

Variables: L B A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L |- ty B}*
============================
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

ty_ignores_ctx < apply IH to H1 H3.

Subgoal 2:

Variables: L B A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L |- ty B}*
H5 : {ty A1}
============================
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

ty_ignores_ctx < apply IH to H1 H4.

Subgoal 2:

Variables: L B A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L |- ty B}*
H5 : {ty A1}
H6 : {ty B}
============================
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

ty_ignores_ctx < search.

Subgoal 3:

Variables: L A F
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L, [F] |- ty A}*
H4 : member F L
============================
 {ty A}

ty_ignores_ctx < apply ctx_member to H1 H4.

Subgoal 3:

Variables: L A X A1
IH : forall L A, ctx L -> {L |- ty A}* -> {ty A}
H1 : ctx L
H3 : {L, [of X A1] |- ty A}*
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
 {ty A}

ty_ignores_ctx < case H3.
Proof completed.

Abella < Theorem case_of_app : 
forall L M N B, ctx L -> {L |- of (app M N) B} ->
  (exists A, {L |- of M (arrow A B)} /\ {L |- of N A}).

============================
 forall L M N B, ctx L -> {L |- of (app M N) B} ->
   (exists A, {L |- of M (arrow A B)} /\ {L |- of N A})

case_of_app < intros.

Variables: L M N B
H1 : ctx L
H2 : {L |- of (app M N) B}
============================
 exists A, {L |- of M (arrow A B)} /\ {L |- of N A}

case_of_app < case H2.

Subgoal 1:

Variables: L M N B A
H1 : ctx L
H3 : {L |- of M (arrow A B)}
H4 : {L |- of N A}
============================
 exists A, {L |- of M (arrow A B)} /\ {L |- of N A}

Subgoal 2 is:
 exists A, {L |- of M (arrow A B)} /\ {L |- of N A}

case_of_app < search.

Subgoal 2:

Variables: L M N B F
H1 : ctx L
H3 : {L, [F] |- of (app M N) B}
H4 : member F L
============================
 exists A, {L |- of M (arrow A B)} /\ {L |- of N A}

case_of_app < apply ctx_member to H1 H4.

Subgoal 2:

Variables: L M N B X A
H1 : ctx L
H3 : {L, [of X A] |- of (app M N) B}
H4 : member (of X A) L
H5 : name X
H6 : {ty A}
============================
 exists A, {L |- of M (arrow A B)} /\ {L |- of N A}

case_of_app < case H5.

Subgoal 2:

Variables: L M N B A
H1 : ctx (L n1)
H3 : {L n1, [of n1 A] |- of (app (M n1) (N n1)) B}
H4 : member (of n1 A) (L n1)
H6 : {ty A}
============================
 exists A, {L n1 |- of (M n1) (arrow A B)} /\ {L n1 |- of (N n1) A}

case_of_app < case H3.
Proof completed.

Abella < Theorem case_of_abs : 
forall L M A B, ctx L -> {L |- of (abs A M) B} ->
  (exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})).

============================
 forall L M A B, ctx L -> {L |- of (abs A M) B} ->
   (exists C, B = arrow A C /\ {ty A} /\
        (nabla x, {L, of x A |- of (M x) C}))

case_of_abs < intros.

Variables: L M A B
H1 : ctx L
H2 : {L |- of (abs A M) B}
============================
 exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})

case_of_abs < case H2.

Subgoal 1:

Variables: L M A B1
H1 : ctx L
H3 : {L |- ty A}
H4 : {L, of n1 A |- of (M n1) B1}
============================
 exists C, arrow A B1 = arrow A C /\ {ty A} /\
   (nabla x, {L, of x A |- of (M x) C})

Subgoal 2 is:
 exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})

case_of_abs < apply ty_ignores_ctx to H1 H3.

Subgoal 1:

Variables: L M A B1
H1 : ctx L
H3 : {L |- ty A}
H4 : {L, of n1 A |- of (M n1) B1}
H5 : {ty A}
============================
 exists C, arrow A B1 = arrow A C /\ {ty A} /\
   (nabla x, {L, of x A |- of (M x) C})

Subgoal 2 is:
 exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})

case_of_abs < search.

Subgoal 2:

Variables: L M A B F
H1 : ctx L
H3 : {L, [F] |- of (abs A M) B}
H4 : member F L
============================
 exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})

case_of_abs < apply ctx_member to H1 H4.

Subgoal 2:

Variables: L M A B X A1
H1 : ctx L
H3 : {L, [of X A1] |- of (abs A M) B}
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
 exists C, B = arrow A C /\ {ty A} /\ (nabla x, {L, of x A |- of (M x) C})

case_of_abs < case H5.

Subgoal 2:

Variables: L M A B A1
H1 : ctx (L n1)
H3 : {L n1, [of n1 A1] |- of (abs A (M n1)) B}
H4 : member (of n1 A1) (L n1)
H6 : {ty A1}
============================
 exists C, B = arrow A C /\ {ty A} /\
   (nabla x, {L n1, of x A |- of (M n1 x) C})

case_of_abs < case H3.
Proof completed.

Abella < Theorem of_step_ext : 
forall L M N A, ctx L -> {L |- of M A} -> {step M N} -> {L |- of N A}.

============================
 forall L M N A, ctx L -> {L |- of M A} -> {step M N} -> {L |- of N A}

of_step_ext < induction on 3.

IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
============================
 forall L M N A, ctx L -> {L |- of M A} -> {step M N}@ -> {L |- of N A}

of_step_ext < intros.

Variables: L M N A
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of M A}
H3 : {step M N}@
============================
 {L |- of N A}

of_step_ext < case H3.

Subgoal 1:

Variables: L A M' M1 N1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step M1 M'}*
============================
 {L |- of (app M' N1) A}

Subgoal 2 is:
 {L |- of (app M1 N') A}

Subgoal 3 is:
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < apply case_of_app to H1 H2.

Subgoal 1:

Variables: L A M' M1 N1 A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step M1 M'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
============================
 {L |- of (app M' N1) A}

Subgoal 2 is:
 {L |- of (app M1 N') A}

Subgoal 3 is:
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < apply IH to H1 H5 H4.

Subgoal 1:

Variables: L A M' M1 N1 A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step M1 M'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
H7 : {L |- of M' (arrow A1 A)}
============================
 {L |- of (app M' N1) A}

Subgoal 2 is:
 {L |- of (app M1 N') A}

Subgoal 3 is:
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < search.

Subgoal 2:

Variables: L A N' N1 M1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step N1 N'}*
============================
 {L |- of (app M1 N') A}

Subgoal 3 is:
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < apply case_of_app to H1 H2.

Subgoal 2:

Variables: L A N' N1 M1 A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step N1 N'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
============================
 {L |- of (app M1 N') A}

Subgoal 3 is:
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < apply IH to H1 H6 H4.

Subgoal 2:

Variables: L A N' N1 M1 A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app M1 N1) A}
H4 : {step N1 N'}*
H5 : {L |- of M1 (arrow A1 A)}
H6 : {L |- of N1 A1}
H7 : {L |- of N' A1}
============================
 {L |- of (app M1 N') A}

Subgoal 3 is:
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < search.

Subgoal 3:

Variables: L A M1 R A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) A}
============================
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < apply case_of_app to H1 H2.

Subgoal 3:

Variables: L A M1 R A1 A2
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) A}
H4 : {L |- of (abs A1 R) (arrow A2 A)}
H5 : {L |- of M1 A2}
============================
 {L |- of (R M1) A}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < apply case_of_abs to H1 H4.

Subgoal 3:

Variables: L M1 R A1 C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {ty A1}
H7 : {L, of n1 A1 |- of (R n1) C}
============================
 {L |- of (R M1) C}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext <  inst H7 with n1 = M1.

Subgoal 3:

Variables: L M1 R A1 C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {ty A1}
H7 : {L, of n1 A1 |- of (R n1) C}
H8 : {L, of M1 A1 |- of (R M1) C}
============================
 {L |- of (R M1) C}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < cut H8 with H5.

Subgoal 3:

Variables: L M1 R A1 C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (app (abs A1 R) M1) C}
H4 : {L |- of (abs A1 R) (arrow A1 C)}
H5 : {L |- of M1 A1}
H6 : {ty A1}
H7 : {L, of n1 A1 |- of (R n1) C}
H8 : {L, of M1 A1 |- of (R M1) C}
H9 : {L |- of (R M1) C}
============================
 {L |- of (R M1) C}

Subgoal 4 is:
 {L |- of (abs A1 R') A}

of_step_ext < search.

Subgoal 4:

Variables: L A R' R A1
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (abs A1 R) A}
H4 : {step (R n1) (R' n1)}*
============================
 {L |- of (abs A1 R') A}

of_step_ext < apply case_of_abs to H1 H2.

Subgoal 4:

Variables: L R' R A1 C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (abs A1 R) (arrow A1 C)}
H4 : {step (R n1) (R' n1)}*
H5 : {ty A1}
H6 : {L, of n1 A1 |- of (R n1) C}
============================
 {L |- of (abs A1 R') (arrow A1 C)}

of_step_ext < apply IH to _ H6 H4.

Subgoal 4:

Variables: L R' R A1 C
IH : forall L M N A, ctx L -> {L |- of M A} -> {step M N}* -> {L |- of N A}
H1 : ctx L
H2 : {L |- of (abs A1 R) (arrow A1 C)}
H4 : {step (R n1) (R' n1)}*
H5 : {ty A1}
H6 : {L, of n1 A1 |- of (R n1) C}
H7 : {L, of n1 A1 |- of (R' n1) C}
============================
 {L |- of (abs A1 R') (arrow A1 C)}

of_step_ext < search.
Proof completed.

Abella < Theorem of_step : 
forall M N A, {of M A} -> {step M N} -> {of N A}.

============================
 forall M N A, {of M A} -> {step M N} -> {of N A}

of_step < intros.

Variables: M N A
H1 : {of M A}
H2 : {step M N}
============================
 {of N A}

of_step < apply of_step_ext to _ H1 H2.

Variables: M N A
H1 : {of M A}
H2 : {step M N}
H3 : {of N A}
============================
 {of N A}

of_step < search.
Proof completed.

Abella < Theorem sn_step : 
forall M N, sn M -> {step M N} -> sn N.

============================
 forall M N, sn M -> {step M N} -> sn N

sn_step < intros.

Variables: M N
H1 : sn M
H2 : {step M N}
============================
 sn N

sn_step < case H1.

Variables: M N
H2 : {step M N}
H3 : forall N, {step M N} -> sn N
============================
 sn N

sn_step < apply H3 to H2.

Variables: M N
H2 : {step M N}
H3 : forall N, {step M N} -> sn N
H4 : sn N
============================
 sn N

sn_step < search.
Proof completed.

Abella < Theorem reduce_step : 
forall M N A, reduce M A -> {step M N} -> reduce N A.

============================
 forall M N A, reduce M A -> {step M N} -> reduce N A

reduce_step < induction on 1.

IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
============================
 forall M N A, reduce M A @ -> {step M N} -> reduce N A

reduce_step < intros.

Variables: M N A
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H1 : reduce M A @
H2 : {step M N}
============================
 reduce N A

reduce_step < case H1.

Subgoal 1:

Variables: M N
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M top}
H4 : sn M
============================
 reduce N top

Subgoal 2 is:
 reduce N (arrow A1 B)

reduce_step < apply of_step to H3 H2.

Subgoal 1:

Variables: M N
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M top}
H4 : sn M
H5 : {of N top}
============================
 reduce N top

Subgoal 2 is:
 reduce N (arrow A1 B)

reduce_step < apply sn_step to H4 H2.

Subgoal 1:

Variables: M N
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M top}
H4 : sn M
H5 : {of N top}
H6 : sn N
============================
 reduce N top

Subgoal 2 is:
 reduce N (arrow A1 B)

reduce_step < search.

Subgoal 2:

Variables: M N B A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
============================
 reduce N (arrow A1 B)

reduce_step < unfold.

Subgoal 2.1:

Variables: M N B A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
============================
 {of N (arrow A1 B)}

Subgoal 2.2 is:
 forall U, reduce U A1 -> reduce (app N U) B

reduce_step < apply of_step to H3 H2.

Subgoal 2.1:

Variables: M N B A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : {of N (arrow A1 B)}
============================
 {of N (arrow A1 B)}

Subgoal 2.2 is:
 forall U, reduce U A1 -> reduce (app N U) B

reduce_step < search.

Subgoal 2.2:

Variables: M N B A1
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
============================
 forall U, reduce U A1 -> reduce (app N U) B

reduce_step < intros.

Subgoal 2.2:

Variables: M N B A1 U
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : reduce U A1
============================
 reduce (app N U) B

reduce_step < apply H4 to H5.

Subgoal 2.2:

Variables: M N B A1 U
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : reduce U A1
H6 : reduce (app M U) B *
============================
 reduce (app N U) B

reduce_step < apply IH to H6 _.

Subgoal 2.2:

Variables: M N B A1 U
IH : forall M N A, reduce M A * -> {step M N} -> reduce N A
H2 : {step M N}
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B *
H5 : reduce U A1
H6 : reduce (app M U) B *
H7 : reduce (app N U) B
============================
 reduce (app N U) B

reduce_step < search.
Proof completed.

Abella < Theorem sn_app_c : 
forall M, sn (app M c) -> sn M.

============================
 forall M, sn (app M c) -> sn M

sn_app_c < induction on 1.

IH : forall M, sn (app M c) * -> sn M
============================
 forall M, sn (app M c) @ -> sn M

sn_app_c < intros.

Variables: M
IH : forall M, sn (app M c) * -> sn M
H1 : sn (app M c) @
============================
 sn M

sn_app_c < case H1.

Variables: M
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
============================
 sn M

sn_app_c < unfold.

Variables: M
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
============================
 forall N, {step M N} -> sn N

sn_app_c < intros.

Variables: M N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
============================
 sn N

sn_app_c < assert {step (app M c) (app N c)}.

Variables: M N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
H4 : {step (app M c) (app N c)}
============================
 sn N

sn_app_c < apply H2 to H4.

Variables: M N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
H4 : {step (app M c) (app N c)}
H5 : sn (app N c) *
============================
 sn N

sn_app_c < apply IH to H5.

Variables: M N
IH : forall M, sn (app M c) * -> sn M
H2 : forall N, {step (app M c) N} -> sn N *
H3 : {step M N}
H4 : {step (app M c) (app N c)}
H5 : sn (app N c) *
H6 : sn N
============================
 sn N

sn_app_c < search.
Proof completed.

Abella < Theorem cr1_cr3 : 
forall A, {ty A} -> (forall M, reduce M A -> sn M) /\
  (forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
       reduce M A).

============================
 forall A, {ty A} -> (forall M, reduce M A -> sn M) /\
   (forall M, neutral M -> {of M A} ->
        (forall P, {step M P} -> reduce P A) -> reduce M A)

cr1_cr3 < induction on 1.

IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
============================
 forall A, {ty A}@ -> (forall M, reduce M A -> sn M) /\
   (forall M, neutral M -> {of M A} ->
        (forall P, {step M P} -> reduce P A) -> reduce M A)

cr1_cr3 < intros.

Variables: A
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
============================
 (forall M, reduce M A -> sn M) /\
   (forall M, neutral M -> {of M A} ->
        (forall P, {step M P} -> reduce P A) -> reduce M A)

cr1_cr3 < split*.

Subgoal 1:

Variables: A
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
============================
 forall M, reduce M A -> sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < intros.

Subgoal 1:

Variables: A M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
H2 : reduce M A
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < case H2.

Subgoal 1.1:

Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty top}@
H3 : {of M top}
H4 : sn M
============================
 sn M

Subgoal 1.2 is:
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < search.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty (arrow A1 B)}@
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < case H1.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < assert neutral c.

Subgoal 1.2.1:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
============================
 neutral c

Subgoal 1.2 is:
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < unfold.

Subgoal 1.2.1:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
============================
 forall A R, c = abs A R -> false

Subgoal 1.2 is:
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < intros.

Subgoal 1.2.1:

Variables: M B A1 A2 R
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : c = abs A2 R
============================
 false

Subgoal 1.2 is:
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < case H7.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < assert {of c A1}.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < assert forall P, {step c P} -> reduce P A1.

Subgoal 1.2.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
============================
 forall P, {step c P} -> reduce P A1

Subgoal 1.2 is:
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < intros.

Subgoal 1.2.2:

Variables: M B A1 P
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : {step c P}
============================
 reduce P A1

Subgoal 1.2 is:
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < case H9.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < apply IH to H5.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < apply H11 to H7 H8 H9.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < apply H4 to H12.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < apply IH to H6.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
H14 : forall M, reduce M B -> sn M
H15 : forall M, neutral M -> {of M B} ->
        (forall P, {step M P} -> reduce P B) -> reduce M B
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < apply H14 to H13.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
H14 : forall M, reduce M B -> sn M
H15 : forall M, neutral M -> {of M B} ->
        (forall P, {step M P} -> reduce P B) -> reduce M B
H16 : sn (app M c)
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < apply sn_app_c to H16.

Subgoal 1.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H3 : {of M (arrow A1 B)}
H4 : forall U, reduce U A1 -> reduce (app M U) B
H5 : {ty A1}*
H6 : {ty B}*
H7 : neutral c
H8 : {of c A1}
H9 : forall P, {step c P} -> reduce P A1
H10 : forall M, reduce M A1 -> sn M
H11 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H12 : reduce c A1
H13 : reduce (app M c) B
H14 : forall M, reduce M B -> sn M
H15 : forall M, neutral M -> {of M B} ->
        (forall P, {step M P} -> reduce P B) -> reduce M B
H16 : sn (app M c)
H17 : sn M
============================
 sn M

Subgoal 2 is:
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < search.

Subgoal 2:

Variables: A
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
H2 : forall M, reduce M A -> sn M
============================
 forall M, neutral M -> {of M A} -> (forall P, {step M P} -> reduce P A) ->
   reduce M A

cr1_cr3 < intros.

Subgoal 2:

Variables: A M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H1 : {ty A}@
H2 : forall M, reduce M A -> sn M
H3 : neutral M
H4 : {of M A}
H5 : forall P, {step M P} -> reduce P A
============================
 reduce M A

cr1_cr3 < case H1.

Subgoal 2.1:

Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
 reduce M top

Subgoal 2.2 is:
 reduce M (arrow A1 B)

cr1_cr3 < unfold.

Subgoal 2.1.1:

Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
 {of M top}

Subgoal 2.1.2 is:
 sn M

Subgoal 2.2 is:
 reduce M (arrow A1 B)

cr1_cr3 < search.

Subgoal 2.1.2:

Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
 sn M

Subgoal 2.2 is:
 reduce M (arrow A1 B)

cr1_cr3 < unfold.

Subgoal 2.1.2:

Variables: M
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
============================
 forall N, {step M N} -> sn N

Subgoal 2.2 is:
 reduce M (arrow A1 B)

cr1_cr3 < intros.

Subgoal 2.1.2:

Variables: M N
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
============================
 sn N

Subgoal 2.2 is:
 reduce M (arrow A1 B)

cr1_cr3 < apply H5 to H6.

Subgoal 2.1.2:

Variables: M N
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
H7 : reduce N top
============================
 sn N

Subgoal 2.2 is:
 reduce M (arrow A1 B)

cr1_cr3 < apply H2 to H7.

Subgoal 2.1.2:

Variables: M N
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M top -> sn M
H3 : neutral M
H4 : {of M top}
H5 : forall P, {step M P} -> reduce P top
H6 : {step M N}
H7 : reduce N top
H8 : sn N
============================
 sn N

Subgoal 2.2 is:
 reduce M (arrow A1 B)

cr1_cr3 < search.

Subgoal 2.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
============================
 reduce M (arrow A1 B)

cr1_cr3 < unfold.

Subgoal 2.2.1:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
============================
 {of M (arrow A1 B)}

Subgoal 2.2.2 is:
 forall U, reduce U A1 -> reduce (app M U) B

cr1_cr3 < search.

Subgoal 2.2.2:

Variables: M B A1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
============================
 forall U, reduce U A1 -> reduce (app M U) B

cr1_cr3 < intros.

Subgoal 2.2.2:

Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
============================
 reduce (app M U) B

cr1_cr3 < apply IH to H6.

Subgoal 2.2.2:

Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
============================
 reduce (app M U) B

cr1_cr3 < apply H9 to H8.

Subgoal 2.2.2:

Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
============================
 reduce (app M U) B

cr1_cr3 < assert forall U, sn U -> reduce U A1 -> reduce (app M U) B.

Subgoal 2.2.2.1:

Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
============================
 forall U, sn U -> reduce U A1 -> reduce (app M U) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < induction on 1.

Subgoal 2.2.2.1:

Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
============================
 forall U, sn U @@ -> reduce U A1 -> reduce (app M U) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < intros.

Subgoal 2.2.2.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H12 : sn U1 @@
H13 : reduce U1 A1
============================
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < case H12.

Subgoal 2.2.2.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
============================
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < assert forall P, {step (app M U1) P} -> reduce P B.

Subgoal 2.2.2.1.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
============================
 forall P, {step (app M U1) P} -> reduce P B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < intros.

Subgoal 2.2.2.1.1:

Variables: M B A1 U U1 P
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : {step (app M U1) P}
============================
 reduce P B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < case H15.

Subgoal 2.2.2.1.1.1:

Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
============================
 reduce (app M' U1) B

Subgoal 2.2.2.1.1.2 is:
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply H5 to H16.

Subgoal 2.2.2.1.1.1:

Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
H17 : reduce M' (arrow A1 B)
============================
 reduce (app M' U1) B

Subgoal 2.2.2.1.1.2 is:
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < case H17.

Subgoal 2.2.2.1.1.1:

Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
H18 : {of M' (arrow A1 B)}
H19 : forall U, reduce U A1 -> reduce (app M' U) B
============================
 reduce (app M' U1) B

Subgoal 2.2.2.1.1.2 is:
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply H19 to H13.

Subgoal 2.2.2.1.1.1:

Variables: M B A1 U U1 M'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step M M'}
H18 : {of M' (arrow A1 B)}
H19 : forall U, reduce U A1 -> reduce (app M' U) B
H20 : reduce (app M' U1) B
============================
 reduce (app M' U1) B

Subgoal 2.2.2.1.1.2 is:
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < search.

Subgoal 2.2.2.1.1.2:

Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
============================
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply H14 to H16.

Subgoal 2.2.2.1.1.2:

Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
H17 : sn N' **
============================
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply reduce_step to H13 H16.

Subgoal 2.2.2.1.1.2:

Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
H17 : sn N' **
H18 : reduce N' A1
============================
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply IH1 to H17 H18.

Subgoal 2.2.2.1.1.2:

Variables: M B A1 U U1 N'
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : {step U1 N'}
H17 : sn N' **
H18 : reduce N' A1
H19 : reduce (app M N') B
============================
 reduce (app M N') B

Subgoal 2.2.2.1.1.3 is:
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < search.

Subgoal 2.2.2.1.1.3:

Variables: B A1 U U1 R A2
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral (abs A2 R)
H4 : {of (abs A2 R) (arrow A1 B)}
H5 : forall P, {step (abs A2 R) P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app (abs A2 R) U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
============================
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < case H3.

Subgoal 2.2.2.1.1.3:

Variables: B A1 U U1 R A2
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H4 : {of (abs A2 R) (arrow A1 B)}
H5 : forall P, {step (abs A2 R) P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app (abs A2 R) U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H16 : forall A R1, abs A2 R = abs A R1 -> false
============================
 reduce (R U1) B

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply H16 to _.

Subgoal 2.2.2.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
============================
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < assert neutral (app M U1).

Subgoal 2.2.2.1.2:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
============================
 neutral (app M U1)

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < unfold.

Subgoal 2.2.2.1.2:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
============================
 forall A R, app M U1 = abs A R -> false

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < intros.

Subgoal 2.2.2.1.2:

Variables: M B A1 U U1 A2 R
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : app M U1 = abs A2 R
============================
 false

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < case H16.

Subgoal 2.2.2.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
============================
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < assert {of (app M U1) B}.

Subgoal 2.2.2.1.3:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
============================
 {of (app M U1) B}

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply reduce_of to H13.

Subgoal 2.2.2.1.3:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of U1 A1}
============================
 {of (app M U1) B}

Subgoal 2.2.2.1 is:
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < search.

Subgoal 2.2.2.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of (app M U1) B}
============================
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply IH to H7.

Subgoal 2.2.2.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of (app M U1) B}
H18 : forall M, reduce M B -> sn M
H19 : forall M, neutral M -> {of M B} ->
        (forall P, {step M P} -> reduce P B) -> reduce M B
============================
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < apply H19 to H16 H17 H15.

Subgoal 2.2.2.1:

Variables: M B A1 U U1
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
IH1 : forall U, sn U ** -> reduce U A1 -> reduce (app M U) B
H13 : reduce U1 A1
H14 : forall N, {step U1 N} -> sn N **
H15 : forall P, {step (app M U1) P} -> reduce P B
H16 : neutral (app M U1)
H17 : {of (app M U1) B}
H18 : forall M, reduce M B -> sn M
H19 : forall M, neutral M -> {of M B} ->
        (forall P, {step M P} -> reduce P B) -> reduce M B
H20 : reduce (app M U1) B
============================
 reduce (app M U1) B

Subgoal 2.2.2 is:
 reduce (app M U) B

cr1_cr3 < search.

Subgoal 2.2.2:

Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
H12 : forall U, sn U -> reduce U A1 -> reduce (app M U) B
============================
 reduce (app M U) B

cr1_cr3 < apply H12 to H11 H8.

Subgoal 2.2.2:

Variables: M B A1 U
IH : forall A, {ty A}* -> (forall M, reduce M A -> sn M) /\
       (forall M, neutral M -> {of M A} ->
            (forall P, {step M P} -> reduce P A) -> reduce M A)
H2 : forall M, reduce M (arrow A1 B) -> sn M
H3 : neutral M
H4 : {of M (arrow A1 B)}
H5 : forall P, {step M P} -> reduce P (arrow A1 B)
H6 : {ty A1}*
H7 : {ty B}*
H8 : reduce U A1
H9 : forall M, reduce M A1 -> sn M
H10 : forall M, neutral M -> {of M A1} ->
        (forall P, {step M P} -> reduce P A1) -> reduce M A1
H11 : sn U
H12 : forall U, sn U -> reduce U A1 -> reduce (app M U) B
H13 : reduce (app M U) B
============================
 reduce (app M U) B

cr1_cr3 < search.
Proof completed.

Abella < Theorem reduce_sn : 
forall A M, {ty A} -> reduce M A -> sn M.

============================
 forall A M, {ty A} -> reduce M A -> sn M

reduce_sn < intros.

Variables: A M
H1 : {ty A}
H2 : reduce M A
============================
 sn M

reduce_sn < apply cr1_cr3 to H1.

Variables: A M
H1 : {ty A}
H2 : reduce M A
H3 : forall M, reduce M A -> sn M
H4 : forall M, neutral M -> {of M A} ->
       (forall P, {step M P} -> reduce P A) -> reduce M A
============================
 sn M

reduce_sn < apply H3 to H2.

Variables: A M
H1 : {ty A}
H2 : reduce M A
H3 : forall M, reduce M A -> sn M
H4 : forall M, neutral M -> {of M A} ->
       (forall P, {step M P} -> reduce P A) -> reduce M A
H5 : sn M
============================
 sn M

reduce_sn < search.
Proof completed.

Abella < Theorem neutral_step_reduce : 
forall A M, neutral M -> {of M A} -> {ty A} ->
  (forall P, {step M P} -> reduce P A) -> reduce M A.

============================
 forall A M, neutral M -> {of M A} -> {ty A} ->
   (forall P, {step M P} -> reduce P A) -> reduce M A

neutral_step_reduce < intros.

Variables: A M
H1 : neutral M
H2 : {of M A}
H3 : {ty A}
H4 : forall P, {step M P} -> reduce P A
============================
 reduce M A

neutral_step_reduce < apply cr1_cr3 to H3.

Variables: A M
H1 : neutral M
H2 : {of M A}
H3 : {ty A}
H4 : forall P, {step M P} -> reduce P A
H5 : forall M, reduce M A -> sn M
H6 : forall M, neutral M -> {of M A} ->
       (forall P, {step M P} -> reduce P A) -> reduce M A
============================
 reduce M A

neutral_step_reduce < apply H6 to H1 H2 H4.

Variables: A M
H1 : neutral M
H2 : {of M A}
H3 : {ty A}
H4 : forall P, {step M P} -> reduce P A
H5 : forall M, reduce M A -> sn M
H6 : forall M, neutral M -> {of M A} ->
       (forall P, {step M P} -> reduce P A) -> reduce M A
H7 : reduce M A
============================
 reduce M A

neutral_step_reduce < search.
Proof completed.

Abella < Theorem of_ty_ext : 
forall L M A, ctx L -> {L |- of M A} -> {ty A}.

============================
 forall L M A, ctx L -> {L |- of M A} -> {ty A}

of_ty_ext < induction on 2.

IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
============================
 forall L M A, ctx L -> {L |- of M A}@ -> {ty A}

of_ty_ext < intros.

Variables: L M A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H2 : {L |- of M A}@
============================
 {ty A}

of_ty_ext < case H2.

Subgoal 1:

Variables: L A A1 N M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
============================
 {ty A}

Subgoal 2 is:
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < apply IH to H1 H3.

Subgoal 1:

Variables: L A A1 N M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
H5 : {ty (arrow A1 A)}
============================
 {ty A}

Subgoal 2 is:
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < case H5.

Subgoal 1:

Variables: L A A1 N M1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of N A1}*
H6 : {ty A1}
H7 : {ty A}
============================
 {ty A}

Subgoal 2 is:
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < search.

Subgoal 2:

Variables: L B R A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
============================
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < apply ty_ignores_ctx to H1 H3.

Subgoal 2:

Variables: L B R A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
H5 : {ty A1}
============================
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < apply IH to _ H4.

Subgoal 2:

Variables: L B R A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n1 A1 |- of (R n1) B}*
H5 : {ty A1}
H6 : {ty B}
============================
 {ty (arrow A1 B)}

Subgoal 3 is:
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < search.

Subgoal 3:

Variables: L A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A}*
============================
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < apply ty_ignores_ctx to H1 H3.

Subgoal 3:

Variables: L A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L |- ty A}*
H4 : {ty A}
============================
 {ty A}

Subgoal 4 is:
 {ty A}

of_ty_ext < search.

Subgoal 4:

Variables: L M A F
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L, [F] |- of M A}*
H4 : member F L
============================
 {ty A}

of_ty_ext < apply ctx_member to H1 H4.

Subgoal 4:

Variables: L M A X A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx L
H3 : {L, [of X A1] |- of M A}*
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
 {ty A}

of_ty_ext < case H5.

Subgoal 4:

Variables: L M A A1
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx (L n1)
H3 : {L n1, [of n1 A1] |- of (M n1) A}*
H4 : member (of n1 A1) (L n1)
H6 : {ty A1}
============================
 {ty A}

of_ty_ext < case H3.

Subgoal 4:

Variables: L A
IH : forall L M A, ctx L -> {L |- of M A}* -> {ty A}
H1 : ctx (L n1)
H4 : member (of n1 A) (L n1)
H6 : {ty A}
============================
 {ty A}

of_ty_ext < search.
Proof completed.

Abella < Theorem of_ty : 
forall M A, {of M A} -> {ty A}.

============================
 forall M A, {of M A} -> {ty A}

of_ty < intros.

Variables: M A
H1 : {of M A}
============================
 {ty A}

of_ty < apply of_ty_ext to _ H1.

Variables: M A
H1 : {of M A}
H2 : {ty A}
============================
 {ty A}

of_ty < search.
Proof completed.

Abella < Theorem reduce_const : 
forall C, {ty C} -> reduce c C.

============================
 forall C, {ty C} -> reduce c C

reduce_const < intros.

Variables: C
H1 : {ty C}
============================
 reduce c C

reduce_const < assert neutral c.

Subgoal 1:

Variables: C
H1 : {ty C}
============================
 neutral c

Subgoal is:
 reduce c C

reduce_const < unfold.

Subgoal 1:

Variables: C
H1 : {ty C}
============================
 forall A R, c = abs A R -> false

Subgoal is:
 reduce c C

reduce_const < intros.

Subgoal 1:

Variables: C A R
H1 : {ty C}
H2 : c = abs A R
============================
 false

Subgoal is:
 reduce c C

reduce_const < case H2.

Variables: C
H1 : {ty C}
H2 : neutral c
============================
 reduce c C

reduce_const < assert forall P, {step c P} -> reduce P C.

Subgoal 2:

Variables: C
H1 : {ty C}
H2 : neutral c
============================
 forall P, {step c P} -> reduce P C

Subgoal is:
 reduce c C

reduce_const < intros.

Subgoal 2:

Variables: C P
H1 : {ty C}
H2 : neutral c
H3 : {step c P}
============================
 reduce P C

Subgoal is:
 reduce c C

reduce_const < case H3.

Variables: C
H1 : {ty C}
H2 : neutral c
H3 : forall P, {step c P} -> reduce P C
============================
 reduce c C

reduce_const < apply neutral_step_reduce to H2 _ H1 H3.

Variables: C
H1 : {ty C}
H2 : neutral c
H3 : forall P, {step c P} -> reduce P C
H4 : reduce c C
============================
 reduce c C

reduce_const < search.
Proof completed.

Abella < Theorem abs_step_reduce_lemma : 
forall U M A B, sn U -> sn (M c) -> reduce U A ->
  (forall V, reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
  reduce (app (abs A M) U) B.

============================
 forall U M A B, sn U -> sn (M c) -> reduce U A ->
   (forall V, reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
   reduce (app (abs A M) U) B

abs_step_reduce_lemma < induction on 1.

IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
============================
 forall U M A B, sn U @ -> sn (M c) -> reduce U A ->
   (forall V, reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
   reduce (app (abs A M) U) B

abs_step_reduce_lemma < induction on 2.

IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
============================
 forall U M A B, sn U @ -> sn (M c) @@ -> reduce U A ->
   (forall V, reduce V A -> reduce (M V) B) -> {of (abs A M) (arrow A B)} ->
   reduce (app (abs A M) U) B

abs_step_reduce_lemma < intros.

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
============================
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < assert forall P, {step (app (abs A M) U) P} -> reduce P B.

Subgoal 1:

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
============================
 forall P, {step (app (abs A M) U) P} -> reduce P B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < intros.

Subgoal 1:

Variables: U M A B P
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : {step (app (abs A M) U) P}
============================
 reduce P B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < case H6.

Subgoal 1.1:

Variables: U M A B M'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step (abs A M) M'}
============================
 reduce (app M' U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < case H7.

Subgoal 1.1:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
============================
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma <  inst H8 with n1 = c.

Subgoal 1.1:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
============================
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < case H2.

Subgoal 1.1:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
============================
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply H10 to H9.

Subgoal 1.1:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
============================
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply IH1 to H1 H11 H3 _ _ with M = R', B = B.

Subgoal 1.1.1:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
============================
 {of (abs A R') (arrow A B)}

Subgoal 1.1.2 is:
 forall V, reduce V A -> reduce (R' V) B

Subgoal 1.1 is:
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply of_step to H5 _.

Subgoal 1.1.1:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : {of (abs A (z1\R' z1)) (arrow A B)}
============================
 {of (abs A R') (arrow A B)}

Subgoal 1.1.2 is:
 forall V, reduce V A -> reduce (R' V) B

Subgoal 1.1 is:
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < search.

Subgoal 1.1.2:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
============================
 forall V, reduce V A -> reduce (R' V) B

Subgoal 1.1 is:
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < intros.

Subgoal 1.1.2:

Variables: U M A B R' V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
============================
 reduce (R' V) B

Subgoal 1.1 is:
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply H4 to H12.

Subgoal 1.1.2:

Variables: U M A B R' V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
H13 : reduce (M V) B
============================
 reduce (R' V) B

Subgoal 1.1 is:
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma <  inst H8 with n1 = V.

Subgoal 1.1.2:

Variables: U M A B R' V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
H13 : reduce (M V) B
H14 : {step (M V) (R' V)}
============================
 reduce (R' V) B

Subgoal 1.1 is:
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply reduce_step to H13 H14.

Subgoal 1.1.2:

Variables: U M A B R' V
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce V A
H13 : reduce (M V) B
H14 : {step (M V) (R' V)}
H15 : reduce (R' V) B
============================
 reduce (R' V) B

Subgoal 1.1 is:
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < search.

Subgoal 1.1:

Variables: U M A B R'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H8 : {step (M n1) (R' n1)}
H9 : {step (M c) (R' c)}
H10 : forall N, {step (M c) N} -> sn N **
H11 : sn (R' c) **
H12 : reduce (app (abs A R') U) B
============================
 reduce (app (abs A R') U) B

Subgoal 1.2 is:
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < search.

Subgoal 1.2:

Variables: U M A B N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
============================
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < case H1.

Subgoal 1.2:

Variables: U M A B N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
============================
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply H8 to H7.

Subgoal 1.2:

Variables: U M A B N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
H9 : sn N' *
============================
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply reduce_step to H3 H7.

Subgoal 1.2:

Variables: U M A B N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
H9 : sn N' *
H10 : reduce N' A
============================
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply IH to H9 H2 H10 H4 H5 with M = M.

Subgoal 1.2:

Variables: U M A B N'
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : {step U N'}
H8 : forall N, {step U N} -> sn N *
H9 : sn N' *
H10 : reduce N' A
H11 : reduce (app (abs A M) N') B
============================
 reduce (app (abs A M) N') B

Subgoal 1.3 is:
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < search.

Subgoal 1.3:

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
============================
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply H4 to H3.

Subgoal 1.3:

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H7 : reduce (M U) B
============================
 reduce (M U) B

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < search.

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
============================
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < assert neutral (app (abs A M) U).

Subgoal 2:

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
============================
 neutral (app (abs A M) U)

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < unfold.

Subgoal 2:

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
============================
 forall A1 R, app (abs A M) U = abs A1 R -> false

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < intros.

Subgoal 2:

Variables: U M A B A1 R
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : app (abs A M) U = abs A1 R
============================
 false

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < case H7.

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
============================
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < assert {of (app (abs A M) U) B}.

Subgoal 3:

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
============================
 {of (app (abs A M) U) B}

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply reduce_of to H3.

Subgoal 3:

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of U A}
============================
 {of (app (abs A M) U) B}

Subgoal is:
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < search.

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of (app (abs A M) U) B}
============================
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply of_ty to H8.

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of (app (abs A M) U) B}
H9 : {ty B}
============================
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < apply neutral_step_reduce to H7 H8 H9 H6.

Variables: U M A B
IH : forall U M A B, sn U * -> sn (M c) -> reduce U A ->
       (forall V, reduce V A -> reduce (M V) B) ->
       {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
IH1 : forall U M A B, sn U @ -> sn (M c) ** -> reduce U A ->
        (forall V, reduce V A -> reduce (M V) B) ->
        {of (abs A M) (arrow A B)} -> reduce (app (abs A M) U) B
H1 : sn U @
H2 : sn (M c) @@
H3 : reduce U A
H4 : forall V, reduce V A -> reduce (M V) B
H5 : {of (abs A M) (arrow A B)}
H6 : forall P, {step (app (abs A M) U) P} -> reduce P B
H7 : neutral (app (abs A M) U)
H8 : {of (app (abs A M) U) B}
H9 : {ty B}
H10 : reduce (app (abs A M) U) B
============================
 reduce (app (abs A M) U) B

abs_step_reduce_lemma < search.
Proof completed.

Abella < Theorem abs_step_reduce : 
forall M A B, {of (abs A M) (arrow A B)} ->
  (forall V, reduce V A -> reduce (M V) B) -> reduce (abs A M) (arrow A B).

============================
 forall M A B, {of (abs A M) (arrow A B)} ->
   (forall V, reduce V A -> reduce (M V) B) -> reduce (abs A M) (arrow A B)

abs_step_reduce < intros.

Variables: M A B
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
============================
 reduce (abs A M) (arrow A B)

abs_step_reduce < unfold.

Subgoal 1:

Variables: M A B
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
============================
 {of (abs A M) (arrow A B)}

Subgoal 2 is:
 forall U, reduce U A -> reduce (app (abs A M) U) B

abs_step_reduce < search.

Subgoal 2:

Variables: M A B
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
============================
 forall U, reduce U A -> reduce (app (abs A M) U) B

abs_step_reduce < intros.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
============================
 reduce (app (abs A M) U) B

abs_step_reduce < apply of_ty to H1.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H4 : {ty (arrow A B)}
============================
 reduce (app (abs A M) U) B

abs_step_reduce < case H4.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {ty A}
H6 : {ty B}
============================
 reduce (app (abs A M) U) B

abs_step_reduce < apply reduce_const to H5.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {ty A}
H6 : {ty B}
H7 : reduce c A
============================
 reduce (app (abs A M) U) B

abs_step_reduce < apply H2 to H7.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {ty A}
H6 : {ty B}
H7 : reduce c A
H8 : reduce (M c) B
============================
 reduce (app (abs A M) U) B

abs_step_reduce < apply reduce_sn to H5 H3.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {ty A}
H6 : {ty B}
H7 : reduce c A
H8 : reduce (M c) B
H9 : sn U
============================
 reduce (app (abs A M) U) B

abs_step_reduce < apply reduce_sn to H6 H8.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {ty A}
H6 : {ty B}
H7 : reduce c A
H8 : reduce (M c) B
H9 : sn U
H10 : sn (M c)
============================
 reduce (app (abs A M) U) B

abs_step_reduce < apply abs_step_reduce_lemma to H9 H10 H3 H2 H1 with M = M.

Subgoal 2:

Variables: M A B U
H1 : {of (abs A M) (arrow A B)}
H2 : forall V, reduce V A -> reduce (M V) B
H3 : reduce U A
H5 : {ty A}
H6 : {ty B}
H7 : reduce c A
H8 : reduce (M c) B
H9 : sn U
H10 : sn (M c)
H11 : reduce (app (abs A M) U) B
============================
 reduce (app (abs A M) U) B

abs_step_reduce < search.
Proof completed.

Abella < Define closed : tm -> prop by 
closed M := exists A, {of M A}.

Abella < Theorem member_prune : 
forall L E, nabla x, member (E x) L -> (exists F, E = y\F).

============================
 forall L E, nabla x, member (E x) L -> (exists F, E = y\F)

member_prune < induction on 1.

IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
 forall L E, nabla x, member (E x) L @ -> (exists F, E = y\F)

member_prune < intros.

Variables: L E
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
H1 : member (E n1) L @
============================
 exists F, E = y\F

member_prune < case H1.

Subgoal 1:

Variables: L3 L2
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
 exists F, z1\L2 = y\F

Subgoal 2 is:
 exists F, E = y\F

member_prune < search.

Subgoal 2:

Variables: E L3 L2
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member (E n1) L3 *
============================
 exists F, E = y\F

member_prune < apply IH to H2.

Subgoal 2:

Variables: L3 L2 F
IH : forall L E, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member F L3 *
============================
 exists F1, z1\F = y\F1

member_prune < search.
Proof completed.

Abella < Theorem prune_of : 
forall L R A, nabla x, ctx L -> {L |- of (R x) A} -> (exists M, R = y\M).

============================
 forall L R A, nabla x, ctx L -> {L |- of (R x) A} -> (exists M, R = y\M)

prune_of < induction on 2.

IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
============================
 forall L R A, nabla x, ctx L -> {L |- of (R x) A}@ -> (exists M, R = y\M)

prune_of < intros.

Variables: L R A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H2 : {L |- of (R n1) A}@
============================
 exists M, R = y\M

prune_of < case H2.

Subgoal 1:

Variables: L A A1 N M
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L |- of (M n1) (arrow A1 A)}*
H4 : {L |- of (N n1) A1}*
============================
 exists M1, z1\app (M z1) (N z1) = y\M1

Subgoal 2 is:
 exists M, z1\abs A1 (R1 z1) = y\M

Subgoal 3 is:
 exists M, z1\c = y\M

Subgoal 4 is:
 exists M, R = y\M

prune_of < apply IH to H1 H3.

Subgoal 1:

Variables: L A A1 N M1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of (N n1) A1}*
============================
 exists M2, z1\app M1 (N z1) = y\M2

Subgoal 2 is:
 exists M, z1\abs A1 (R1 z1) = y\M

Subgoal 3 is:
 exists M, z1\c = y\M

Subgoal 4 is:
 exists M, R = y\M

prune_of < apply IH to H1 H4.

Subgoal 1:

Variables: L A A1 M1 M2
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L |- of M1 (arrow A1 A)}*
H4 : {L |- of M2 A1}*
============================
 exists M3, z1\app M1 M2 = y\M3

Subgoal 2 is:
 exists M, z1\abs A1 (R1 z1) = y\M

Subgoal 3 is:
 exists M, z1\c = y\M

Subgoal 4 is:
 exists M, R = y\M

prune_of < search.

Subgoal 2:

Variables: L B R1 A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n2 A1 |- of (R1 n1 n2) B}*
============================
 exists M, z1\abs A1 (R1 z1) = y\M

Subgoal 3 is:
 exists M, z1\c = y\M

Subgoal 4 is:
 exists M, R = y\M

prune_of < apply ty_ignores_ctx to H1 H3.

Subgoal 2:

Variables: L B R1 A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n2 A1 |- of (R1 n1 n2) B}*
H5 : {ty A1}
============================
 exists M, z1\abs A1 (R1 z1) = y\M

Subgoal 3 is:
 exists M, z1\c = y\M

Subgoal 4 is:
 exists M, R = y\M

prune_of < apply IH to _ H4.

Subgoal 2:

Variables: L B A1 M
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A1}*
H4 : {L, of n2 A1 |- of (M n2) B}*
H5 : {ty A1}
============================
 exists M1, z1\abs A1 (z2\M z2) = y\M1

Subgoal 3 is:
 exists M, z1\c = y\M

Subgoal 4 is:
 exists M, R = y\M

prune_of < search.

Subgoal 3:

Variables: L A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L |- ty A}*
============================
 exists M, z1\c = y\M

Subgoal 4 is:
 exists M, R = y\M

prune_of < search.

Subgoal 4:

Variables: L R A F
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L, [F n1] |- of (R n1) A}*
H4 : member (F n1) L
============================
 exists M, R = y\M

prune_of < apply member_prune to H4.

Subgoal 4:

Variables: L R A F1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L, [F1] |- of (R n1) A}*
H4 : member F1 L
============================
 exists M, R = y\M

prune_of < apply ctx_member to H1 H4.

Subgoal 4:

Variables: L R A X A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx L
H3 : {L, [of X A1] |- of (R n1) A}*
H4 : member (of X A1) L
H5 : name X
H6 : {ty A1}
============================
 exists M, R = y\M

prune_of < case H5.

Subgoal 4:

Variables: L R A A1
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx (L n2)
H3 : {L n2, [of n2 A1] |- of (R n2 n1) A}*
H4 : member (of n2 A1) (L n2)
H6 : {ty A1}
============================
 exists M, R n2 = y\M

prune_of < case H3.

Subgoal 4:

Variables: L A
IH : forall L R A, nabla x, ctx L -> {L |- of (R x) A}* ->
       (exists M, R = y\M)
H1 : ctx (L n2)
H4 : member (of n2 A) (L n2)
H6 : {ty A}
============================
 exists M, z2\n2 = y\M

prune_of < search.
Proof completed.

Abella < Theorem prune_closed : 
forall R, nabla x, closed (R x) -> (exists M, R = y\M).

============================
 forall R, nabla x, closed (R x) -> (exists M, R = y\M)

prune_closed < intros.

Variables: R
H1 : closed (R n1)
============================
 exists M, R = y\M

prune_closed < case H1.

Variables: R A
H2 : {of (R n1) A}
============================
 exists M, R = y\M

prune_closed < apply prune_of to _ H2.

Variables: A M
H2 : {of M A}
============================
 exists M1, z1\M = y\M1

prune_closed < search.
Proof completed.

Abella < Theorem reduce_closed : 
forall M A, reduce M A -> closed M.

============================
 forall M A, reduce M A -> closed M

reduce_closed < intros.

Variables: M A
H1 : reduce M A
============================
 closed M

reduce_closed < apply reduce_of to H1.

Variables: M A
H1 : reduce M A
H2 : {of M A}
============================
 closed M

reduce_closed < search.
Proof completed.

Abella < Theorem prune_reduce : 
forall R A, nabla x, reduce (R x) A -> (exists M, R = y\M).

============================
 forall R A, nabla x, reduce (R x) A -> (exists M, R = y\M)

prune_reduce < intros.

Variables: R A
H1 : reduce (R n1) A
============================
 exists M, R = y\M

prune_reduce < apply reduce_closed to H1.

Variables: R A
H1 : reduce (R n1) A
H2 : closed (R n1)
============================
 exists M, R = y\M

prune_reduce < apply prune_closed to H2.

Variables: A M
H1 : reduce M A
H2 : closed M
============================
 exists M1, z1\M = y\M1

prune_reduce < search.
Proof completed.

Abella < Define subst : olist -> tm -> tm -> prop by 
subst nil M M;
nabla x, subst (of x A :: L) (R x) M := exists U, reduce U A /\ subst L (R U) M.

Abella < Theorem closed_subst : 
forall L M N, closed M -> subst L M N -> M = N.

============================
 forall L M N, closed M -> subst L M N -> M = N

closed_subst < induction on 2.

IH : forall L M N, closed M -> subst L M N * -> M = N
============================
 forall L M N, closed M -> subst L M N @ -> M = N

closed_subst < intros.

Variables: L M N
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M
H2 : subst L M N @
============================
 M = N

closed_subst < case H2.

Subgoal 1:

Variables: N
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed N
============================
 N = N

Subgoal 2 is:
 M n1 = M1

closed_subst < search.

Subgoal 2:

Variables: M U M1 L1 A
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed (M n1)
H3 : reduce U A
H4 : subst L1 (M U) M1 *
============================
 M n1 = M1

closed_subst < apply prune_closed to H1.

Subgoal 2:

Variables: U M1 L1 A M2
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M2
H3 : reduce U A
H4 : subst L1 M2 M1 *
============================
 M2 = M1

closed_subst < apply IH to H1 H4.

Subgoal 2:

Variables: U M1 L1 A
IH : forall L M N, closed M -> subst L M N * -> M = N
H1 : closed M1
H3 : reduce U A
H4 : subst L1 M1 M1 *
============================
 M1 = M1

closed_subst < search.
Proof completed.

Abella < Theorem subst_const : 
forall L M, subst L c M -> M = c.

============================
 forall L M, subst L c M -> M = c

subst_const < induction on 1.

IH : forall L M, subst L c M * -> M = c
============================
 forall L M, subst L c M @ -> M = c

subst_const < intros.

Variables: L M
IH : forall L M, subst L c M * -> M = c
H1 : subst L c M @
============================
 M = c

subst_const < case H1.

Subgoal 1:

IH : forall L M, subst L c M * -> M = c
============================
 c = c

Subgoal 2 is:
 M1 = c

subst_const < search.

Subgoal 2:

Variables: U M1 L1 A
IH : forall L M, subst L c M * -> M = c
H2 : reduce U A
H3 : subst L1 c M1 *
============================
 M1 = c

subst_const < apply IH to H3.

Subgoal 2:

Variables: U L1 A
IH : forall L M, subst L c M * -> M = c
H2 : reduce U A
H3 : subst L1 c c *
============================
 c = c

subst_const < search.
Proof completed.

Abella < Theorem subst_var : 
forall L M N A, ctx L -> member (of M A) L -> subst L M N -> reduce N A.

============================
 forall L M N A, ctx L -> member (of M A) L -> subst L M N -> reduce N A

subst_var < induction on 1.

IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
============================
 forall L M N A, ctx L @ -> member (of M A) L -> subst L M N -> reduce N A

subst_var < intros.

Variables: L M N A
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H1 : ctx L @
H2 : member (of M A) L
H3 : subst L M N
============================
 reduce N A

subst_var < case H1.

Subgoal 1:

Variables: M N A
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H2 : member (of M A) nil
H3 : subst nil M N
============================
 reduce N A

Subgoal 2 is:
 reduce (N n1) A

subst_var < case H2.

Subgoal 2:

Variables: M N A L1 A1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H2 : member (of (M n1) A) (of n1 A1 :: L1)
H3 : subst (of n1 A1 :: L1) (M n1) (N n1)
H4 : {ty A1}
H5 : ctx L1 *
============================
 reduce (N n1) A

subst_var < case H2.

Subgoal 2.1:

Variables: N L1 A1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H3 : subst (of n1 A1 :: L1) n1 (N n1)
H4 : {ty A1}
H5 : ctx L1 *
============================
 reduce (N n1) A1

Subgoal 2.2 is:
 reduce (N n1) A

subst_var < case H3.

Subgoal 2.1:

Variables: L1 A1 U M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 U M1
============================
 reduce M1 A1

Subgoal 2.2 is:
 reduce (N n1) A

subst_var < apply reduce_closed to H6.

Subgoal 2.1:

Variables: L1 A1 U M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 U M1
H8 : closed U
============================
 reduce M1 A1

Subgoal 2.2 is:
 reduce (N n1) A

subst_var < apply closed_subst to H8 H7.

Subgoal 2.1:

Variables: L1 A1 M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce M1 A1
H7 : subst L1 M1 M1
H8 : closed M1
============================
 reduce M1 A1

Subgoal 2.2 is:
 reduce (N n1) A

subst_var < search.

Subgoal 2.2:

Variables: M N A L1 A1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H3 : subst (of n1 A1 :: L1) (M n1) (N n1)
H4 : {ty A1}
H5 : ctx L1 *
H6 : member (of (M n1) A) L1
============================
 reduce (N n1) A

subst_var < case H3.

Subgoal 2.2:

Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : member (of (M n1) A) L1
H7 : reduce U A1
H8 : subst L1 (M U) M1
============================
 reduce M1 A

subst_var < apply member_prune to H6.

Subgoal 2.2:

Variables: A L1 A1 U M1 F1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : member (of F1 A) L1
H7 : reduce U A1
H8 : subst L1 F1 M1
============================
 reduce M1 A

subst_var < apply IH to H5 H6 H8.

Subgoal 2.2:

Variables: A L1 A1 U M1 F1
IH : forall L M N A, ctx L * -> member (of M A) L -> subst L M N ->
       reduce N A
H4 : {ty A1}
H5 : ctx L1 *
H6 : member (of F1 A) L1
H7 : reduce U A1
H8 : subst L1 F1 M1
H9 : reduce M1 A
============================
 reduce M1 A

subst_var < search.
Proof completed.

Abella < Theorem subst_app : 
forall L M N R, ctx L -> subst L (app M N) R ->
  (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR).

============================
 forall L M N R, ctx L -> subst L (app M N) R ->
   (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)

subst_app < induction on 1.

IH : forall L M N R, ctx L * -> subst L (app M N) R ->
       (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)
============================
 forall L M N R, ctx L @ -> subst L (app M N) R ->
   (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)

subst_app < intros.

Variables: L M N R
IH : forall L M N R, ctx L * -> subst L (app M N) R ->
       (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)
H1 : ctx L @
H2 : subst L (app M N) R
============================
 exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR

subst_app < case H1.

Subgoal 1:

Variables: M N R
IH : forall L M N R, ctx L * -> subst L (app M N) R ->
       (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)
H2 : subst nil (app M N) R
============================
 exists MR NR, R = app MR NR /\ subst nil M MR /\ subst nil N NR

Subgoal 2 is:
 exists MR NR, R n1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
   subst (of n1 A :: L1) (N n1) NR

subst_app < case H2.

Subgoal 1:

Variables: M N
IH : forall L M N R, ctx L * -> subst L (app M N) R ->
       (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)
============================
 exists MR NR, app M N = app MR NR /\ subst nil M MR /\ subst nil N NR

Subgoal 2 is:
 exists MR NR, R n1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
   subst (of n1 A :: L1) (N n1) NR

subst_app < search.

Subgoal 2:

Variables: M N R L1 A
IH : forall L M N R, ctx L * -> subst L (app M N) R ->
       (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)
H2 : subst (of n1 A :: L1) (app (M n1) (N n1)) (R n1)
H3 : {ty A}
H4 : ctx L1 *
============================
 exists MR NR, R n1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
   subst (of n1 A :: L1) (N n1) NR

subst_app < case H2.

Subgoal 2:

Variables: M N L1 A U M1
IH : forall L M N R, ctx L * -> subst L (app M N) R ->
       (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)
H3 : {ty A}
H4 : ctx L1 *
H5 : reduce U A
H6 : subst L1 (app (M U) (N U)) M1
============================
 exists MR NR, M1 = app MR NR /\ subst (of n1 A :: L1) (M n1) MR /\
   subst (of n1 A :: L1) (N n1) NR

subst_app < apply IH to H4 H6.

Subgoal 2:

Variables: M N L1 A U MR NR
IH : forall L M N R, ctx L * -> subst L (app M N) R ->
       (exists MR NR, R = app MR NR /\ subst L M MR /\ subst L N NR)
H3 : {ty A}
H4 : ctx L1 *
H5 : reduce U A
H6 : subst L1 (app (M U) (N U)) (app MR NR)
H7 : subst L1 (M U) MR
H8 : subst L1 (N U) NR
============================
 exists MR1 NR1, app MR NR = app MR1 NR1 /\
   subst (of n1 A :: L1) (M n1) MR1 /\ subst (of n1 A :: L1) (N n1) NR1

subst_app < search.
Proof completed.

Abella < Theorem subst_abs : 
forall L M R A, ctx L -> subst L (abs A M) R -> {ty A} ->
  (exists MR, R = abs A MR /\
       (forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U)))).

============================
 forall L M R A, ctx L -> subst L (abs A M) R -> {ty A} ->
   (exists MR, R = abs A MR /\
        (forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U))))

subst_abs < induction on 1.

IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
============================
 forall L M R A, ctx L @ -> subst L (abs A M) R -> {ty A} ->
   (exists MR, R = abs A MR /\
        (forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U))))

subst_abs < intros.

Variables: L M R A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H1 : ctx L @
H2 : subst L (abs A M) R
H3 : {ty A}
============================
 exists MR, R = abs A MR /\
   (forall U, reduce U A -> (nabla x, subst (of x A :: L) (M x) (MR U)))

subst_abs < case H1.

Subgoal 1:

Variables: M R A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H2 : subst nil (abs A M) R
H3 : {ty A}
============================
 exists MR, R = abs A MR /\
   (forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (MR U)))

Subgoal 2 is:
 exists MR, R n1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < case H2.

Subgoal 1:

Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
 exists MR, abs A M = abs A MR /\
   (forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (MR U)))

Subgoal 2 is:
 exists MR, R n1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < exists M.

Subgoal 1:

Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
 abs A M = abs A M /\
   (forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (M U)))

Subgoal 2 is:
 exists MR, R n1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < split.

Subgoal 1.1:

Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
 abs A M = abs A M

Subgoal 1.2 is:
 forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (M U))

Subgoal 2 is:
 exists MR, R n1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < search.

Subgoal 1.2:

Variables: M A
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
============================
 forall U, reduce U A -> (nabla x, subst (of x A :: nil) (M x) (M U))

Subgoal 2 is:
 exists MR, R n1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < intros.

Subgoal 1.2:

Variables: M A U
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : reduce U A
============================
 subst (of n1 A :: nil) (M n1) (M U)

Subgoal 2 is:
 exists MR, R n1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < search.

Subgoal 2:

Variables: M R A L1 A1
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H2 : subst (of n1 A1 :: L1) (abs A (M n1)) (R n1)
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
============================
 exists MR, R n1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < case H2.

Subgoal 2:

Variables: M A L1 A1 U M1
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) M1
============================
 exists MR, M1 = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < apply IH to H5 H7 H3.

Subgoal 2:

Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
 exists MR1, abs A MR = abs A MR1 /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR1 U)))

subst_abs < exists MR.

Subgoal 2:

Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
 abs A MR = abs A MR /\
   (forall U, reduce U A ->
        (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U)))

subst_abs < split.

Subgoal 2.1:

Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
 abs A MR = abs A MR

Subgoal 2.2 is:
 forall U, reduce U A ->
   (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U))

subst_abs < search.

Subgoal 2.2:

Variables: M A L1 A1 U MR
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
============================
 forall U, reduce U A ->
   (nabla x, subst (of x A :: of n1 A1 :: L1) (M n1 x) (MR U))

subst_abs < intros.

Subgoal 2.2:

Variables: M A L1 A1 U MR U1
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce (U1 n1) A
============================
 subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR (U1 n1))

subst_abs < apply prune_reduce to H9.

Subgoal 2.2:

Variables: M A L1 A1 U MR M2
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce M2 A
============================
 subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR M2)

subst_abs < apply H8 to H9.

Subgoal 2.2:

Variables: M A L1 A1 U MR M2
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce M2 A
H10 : subst (of n1 A :: L1) (M U n1) (MR M2)
============================
 subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR M2)

subst_abs < case H10.

Subgoal 2.2:

Variables: M A L1 A1 U MR M2 U2
IH : forall L M R A, ctx L * -> subst L (abs A M) R -> {ty A} ->
       (exists MR, R = abs A MR /\
            (forall U, reduce U A ->
                 (nabla x, subst (of x A :: L) (M x) (MR U))))
H3 : {ty A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (abs A (M U)) (abs A MR)
H8 : forall U1, reduce U1 A ->
       (nabla x, subst (of x A :: L1) (M U x) (MR U1))
H9 : reduce M2 A
H11 : reduce U2 A
H12 : subst L1 (M U U2) (MR M2)
============================
 subst (of n2 A :: of n1 A1 :: L1) (M n1 n2) (MR M2)

subst_abs < search.
Proof completed.

Abella < Theorem subst_preserves_ty : 
forall L M N A, ctx L -> subst L M N -> {L |- of M A} -> {of N A}.

============================
 forall L M N A, ctx L -> subst L M N -> {L |- of M A} -> {of N A}

subst_preserves_ty < induction on 1.

IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
============================
 forall L M N A, ctx L @ -> subst L M N -> {L |- of M A} -> {of N A}

subst_preserves_ty < intros.

Variables: L M N A
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H1 : ctx L @
H2 : subst L M N
H3 : {L |- of M A}
============================
 {of N A}

subst_preserves_ty < case H1.

Subgoal 1:

Variables: M N A
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H2 : subst nil M N
H3 : {of M A}
============================
 {of N A}

Subgoal 2 is:
 {of (N n1) A}

subst_preserves_ty < case H2.

Subgoal 1:

Variables: N A
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {of N A}
============================
 {of N A}

Subgoal 2 is:
 {of (N n1) A}

subst_preserves_ty < search.

Subgoal 2:

Variables: M N A L1 A1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H2 : subst (of n1 A1 :: L1) (M n1) (N n1)
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
============================
 {of (N n1) A}

subst_preserves_ty < case H2.

Subgoal 2:

Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
============================
 {of M1 A}

subst_preserves_ty < apply reduce_of to H6.

Subgoal 2:

Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
============================
 {of M1 A}

subst_preserves_ty <  inst H3 with n1 = U.

Subgoal 2:

Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
============================
 {of M1 A}

subst_preserves_ty < cut H9 with H8.

Subgoal 2:

Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
H10 : {L1 |- of (M U) A}
============================
 {of M1 A}

subst_preserves_ty < apply of_ty_ext to _ H3.

Subgoal 2:

Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
H10 : {L1 |- of (M U) A}
H11 : {ty A}
============================
 {of M1 A}

subst_preserves_ty < apply IH to H5 H7 H10.

Subgoal 2:

Variables: M A L1 A1 U M1
IH : forall L M N A, ctx L * -> subst L M N -> {L |- of M A} -> {of N A}
H3 : {L1, of n1 A1 |- of (M n1) A}
H4 : {ty A1}
H5 : ctx L1 *
H6 : reduce U A1
H7 : subst L1 (M U) M1
H8 : {of U A1}
H9 : {L1, of U A1 |- of (M U) A}
H10 : {L1 |- of (M U) A}
H11 : {ty A}
H12 : {of M1 A}
============================
 {of M1 A}

subst_preserves_ty < search.
Proof completed.

Abella < Theorem strong_norm_ext : 
forall L M R A, ctx L -> {L |- of M A} -> subst L M R -> reduce R A.

============================
 forall L M R A, ctx L -> {L |- of M A} -> subst L M R -> reduce R A

strong_norm_ext < induction on 2.

IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
============================
 forall L M R A, ctx L -> {L |- of M A}@ -> subst L M R -> reduce R A

strong_norm_ext < intros.

Variables: L M R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of M A}@
H3 : subst L M R
============================
 reduce R A

strong_norm_ext < case H2 (keep).

Subgoal 1:

Variables: L R A A1 N M1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) R
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
============================
 reduce R A

Subgoal 2 is:
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply subst_app to H1 H3.

Subgoal 1:

Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
============================
 reduce (app MR NR) A

Subgoal 2 is:
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply IH to H1 H4 H6.

Subgoal 1:

Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H8 : reduce MR (arrow A1 A)
============================
 reduce (app MR NR) A

Subgoal 2 is:
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply IH to H1 H5 H7.

Subgoal 1:

Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H8 : reduce MR (arrow A1 A)
H9 : reduce NR A1
============================
 reduce (app MR NR) A

Subgoal 2 is:
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < case H8.

Subgoal 1:

Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H9 : reduce NR A1
H10 : {of MR (arrow A1 A)}
H11 : forall U, reduce U A1 -> reduce (app MR U) A
============================
 reduce (app MR NR) A

Subgoal 2 is:
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply H11 to H9.

Subgoal 1:

Variables: L A A1 N M1 MR NR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (app M1 N) A}@
H3 : subst L (app M1 N) (app MR NR)
H4 : {L |- of M1 (arrow A1 A)}*
H5 : {L |- of N A1}*
H6 : subst L M1 MR
H7 : subst L N NR
H9 : reduce NR A1
H10 : {of MR (arrow A1 A)}
H11 : forall U, reduce U A1 -> reduce (app MR U) A
H12 : reduce (app MR NR) A
============================
 reduce (app MR NR) A

Subgoal 2 is:
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < search.

Subgoal 2:

Variables: L R B R1 A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) R
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
============================
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply ty_ignores_ctx to H1 H4.

Subgoal 2:

Variables: L R B R1 A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) R
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
============================
 reduce R (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply subst_abs to H1 H3 H6.

Subgoal 2:

Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
============================
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply subst_preserves_ty to H1 H3 H2.

Subgoal 2:

Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
============================
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply abs_step_reduce to H8 _.

Subgoal 2.1:

Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
============================
 forall V, reduce V A1 -> reduce (MR V) B

Subgoal 2 is:
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < intros.

Subgoal 2.1:

Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
============================
 reduce (MR V) B

Subgoal 2 is:
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply ty_ignores_ctx to H1 H4.

Subgoal 2.1:

Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
H10 : {ty A1}
============================
 reduce (MR V) B

Subgoal 2 is:
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply H7 to H9.

Subgoal 2.1:

Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
H10 : {ty A1}
H11 : subst (of n1 A1 :: L) (R1 n1) (MR V)
============================
 reduce (MR V) B

Subgoal 2 is:
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply IH to _ H5 H11.

Subgoal 2.1:

Variables: L B R1 A1 MR V
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce V A1
H10 : {ty A1}
H11 : subst (of n1 A1 :: L) (R1 n1) (MR V)
H12 : reduce (MR V) B
============================
 reduce (MR V) B

Subgoal 2 is:
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < search.

Subgoal 2:

Variables: L B R1 A1 MR
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of (abs A1 R1) (arrow A1 B)}@
H3 : subst L (abs A1 R1) (abs A1 MR)
H4 : {L |- ty A1}*
H5 : {L, of n1 A1 |- of (R1 n1) B}*
H6 : {ty A1}
H7 : forall U, reduce U A1 -> (nabla x, subst (of x A1 :: L) (R1 x) (MR U))
H8 : {of (abs A1 MR) (arrow A1 B)}
H9 : reduce (abs A1 MR) (arrow A1 B)
============================
 reduce (abs A1 MR) (arrow A1 B)

Subgoal 3 is:
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < search.

Subgoal 3:

Variables: L R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c R
H4 : {L |- ty A}*
============================
 reduce R A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply subst_const to H3.

Subgoal 3:

Variables: L A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c c
H4 : {L |- ty A}*
============================
 reduce c A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply ty_ignores_ctx to H1 H4.

Subgoal 3:

Variables: L A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c c
H4 : {L |- ty A}*
H5 : {ty A}
============================
 reduce c A

Subgoal 4 is:
 reduce R A

strong_norm_ext < apply reduce_const to H5.

Subgoal 3:

Variables: L A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of c A}@
H3 : subst L c c
H4 : {L |- ty A}*
H5 : {ty A}
H6 : reduce c A
============================
 reduce c A

Subgoal 4 is:
 reduce R A

strong_norm_ext < search.

Subgoal 4:

Variables: L M R A F
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of M A}@
H3 : subst L M R
H4 : {L, [F] |- of M A}*
H5 : member F L
============================
 reduce R A

strong_norm_ext < apply ctx_member to H1 H5.

Subgoal 4:

Variables: L M R A X A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx L
H2 : {L |- of M A}@
H3 : subst L M R
H4 : {L, [of X A1] |- of M A}*
H5 : member (of X A1) L
H6 : name X
H7 : {ty A1}
============================
 reduce R A

strong_norm_ext < case H6.

Subgoal 4:

Variables: L M R A A1
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx (L n1)
H2 : {L n1 |- of (M n1) A}@
H3 : subst (L n1) (M n1) (R n1)
H4 : {L n1, [of n1 A1] |- of (M n1) A}*
H5 : member (of n1 A1) (L n1)
H7 : {ty A1}
============================
 reduce (R n1) A

strong_norm_ext < case H4.

Subgoal 4:

Variables: L R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx (L n1)
H2 : {L n1 |- of n1 A}@
H3 : subst (L n1) n1 (R n1)
H5 : member (of n1 A) (L n1)
H7 : {ty A}
============================
 reduce (R n1) A

strong_norm_ext < apply subst_var to H1 H5 H3.

Subgoal 4:

Variables: L R A
IH : forall L M R A, ctx L -> {L |- of M A}* -> subst L M R -> reduce R A
H1 : ctx (L n1)
H2 : {L n1 |- of n1 A}@
H3 : subst (L n1) n1 (R n1)
H5 : member (of n1 A) (L n1)
H7 : {ty A}
H8 : reduce (R n1) A
============================
 reduce (R n1) A

strong_norm_ext < search.
Proof completed.

Abella < Theorem strong_norm : 
forall M A, {of M A} -> sn M.

============================
 forall M A, {of M A} -> sn M

strong_norm < intros.

Variables: M A
H1 : {of M A}
============================
 sn M

strong_norm < apply strong_norm_ext to _ H1 _.

Variables: M A
H1 : {of M A}
H2 : reduce M A
============================
 sn M

strong_norm < apply of_ty to H1.

Variables: M A
H1 : {of M A}
H2 : reduce M A
H3 : {ty A}
============================
 sn M

strong_norm < apply reduce_sn to _ H2.

Variables: M A
H1 : {of M A}
H2 : reduce M A
H3 : {ty A}
H4 : sn M
============================
 sn M

strong_norm < search.
Proof completed.

Abella <