Welcome to Abella 2.0.5-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 0 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 0 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 0 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 0 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 0 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 <