Welcome to Abella 2.0.5-dev.

Abella <Specification "fcurry".Reading specification "fcurry".

Abella <Close ty, tm.

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

============================ forall L E, nabla x, member (E x) L -> (exists F, E = x\F) member_prune <induction on 1.

IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F) ============================ forall L E, nabla x, member (E x) L @ -> (exists F, E = x\F) member_prune <intros.

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

Subgoal 1: Variables: L3 L2 IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F) ============================ exists F, z1\L2 = x\F Subgoal 2 is: exists F, E = x\F member_prune <search.

Subgoal 2: Variables: E L3 L2 IH : forall L E, nabla x, member (E x) L * -> (exists F, E = x\F) H2 : member (E n1) L3 * ============================ exists F, E = x\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 = x\F) H2 : member F L3 * ============================ exists F1, z1\F = x\F1 member_prune <search.Proof completed.

Abella <Define ctx : olist -> prop by ctx nil; nabla x, ctx (of x T :: L) := ctx L.

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

Abella <Theorem of_name : forall L E, ctx L -> member E L -> (exists X T, E = of X T /\ name X).

============================ forall L E, ctx L -> member E L -> (exists X T, E = of X T /\ name X) of_name <induction on 1.

IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) ============================ forall L E, ctx L @ -> member E L -> (exists X T, E = of X T /\ name X) of_name <intros.

Variables: L E IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) H1 : ctx L @ H2 : member E L ============================ exists X T, E = of X T /\ name X of_name <case H1.

Subgoal 1: Variables: E IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) H2 : member E nil ============================ exists X T, E = of X T /\ name X Subgoal 2 is: exists X T, E n1 = of X T /\ name X of_name <case H2.

Subgoal 2: Variables: E L1 T IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) H2 : member (E n1) (of n1 T :: L1) H3 : ctx L1 * ============================ exists X T, E n1 = of X T /\ name X of_name <case H2.

Subgoal 2.1: Variables: L1 T IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) H3 : ctx L1 * ============================ exists X T1, of n1 T = of X T1 /\ name X Subgoal 2.2 is: exists X T, E n1 = of X T /\ name X of_name <search.

Subgoal 2.2: Variables: E L1 T IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) H3 : ctx L1 * H4 : member (E n1) L1 ============================ exists X T, E n1 = of X T /\ name X of_name <apply member_prune to H4.

Subgoal 2.2: Variables: L1 T F IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) H3 : ctx L1 * H4 : member F L1 ============================ exists X T, F = of X T /\ name X of_name <apply IH to H3 H4.

Subgoal 2.2: Variables: L1 T X T1 IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X) H3 : ctx L1 * H4 : member (of X T1) L1 H5 : name X ============================ exists X1 T, of X T1 = of X1 T /\ name X1 of_name <search.Proof completed.

Abella <Theorem ctx_uniq : forall L E T1 T2, ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.

============================ forall L E T1 T2, ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2 ctx_uniq <induction on 1.

IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 ============================ forall L E T1 T2, ctx L @ -> member (of E T1) L -> member (of E T2) L -> T1 = T2 ctx_uniq <intros.

Variables: L E T1 T2 IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H1 : ctx L @ H2 : member (of E T1) L H3 : member (of E T2) L ============================ T1 = T2 ctx_uniq <case H1.

Subgoal 1: Variables: E T1 T2 IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H2 : member (of E T1) nil H3 : member (of E T2) nil ============================ T1 = T2 Subgoal 2 is: T1 = T2 ctx_uniq <case H2.

Subgoal 2: Variables: E T1 T2 L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H2 : member (of (E n1) T1) (of n1 T :: L1) H3 : member (of (E n1) T2) (of n1 T :: L1) H4 : ctx L1 * ============================ T1 = T2 ctx_uniq <case H2.

Subgoal 2.1: Variables: T2 L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H3 : member (of n1 T2) (of n1 T :: L1) H4 : ctx L1 * ============================ T = T2 Subgoal 2.2 is: T1 = T2 ctx_uniq <case H3.

Subgoal 2.1.1: Variables: L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H4 : ctx L1 * ============================ T = T Subgoal 2.1.2 is: T = T2 Subgoal 2.2 is: T1 = T2 ctx_uniq <search.

Subgoal 2.1.2: Variables: T2 L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H4 : ctx L1 * H5 : member (of n1 T2) L1 ============================ T = T2 Subgoal 2.2 is: T1 = T2 ctx_uniq <apply member_prune to H5.

Subgoal 2.2: Variables: E T1 T2 L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H3 : member (of (E n1) T2) (of n1 T :: L1) H4 : ctx L1 * H5 : member (of (E n1) T1) L1 ============================ T1 = T2 ctx_uniq <case H3.

Subgoal 2.2.1: Variables: T1 L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H4 : ctx L1 * H5 : member (of n1 T1) L1 ============================ T1 = T Subgoal 2.2.2 is: T1 = T2 ctx_uniq <apply member_prune to H5.

Subgoal 2.2.2: Variables: E T1 T2 L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H4 : ctx L1 * H5 : member (of (E n1) T1) L1 H6 : member (of (E n1) T2) L1 ============================ T1 = T2 ctx_uniq <apply IH to H4 H5 H6.

Subgoal 2.2.2: Variables: E T2 L1 T IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L -> T1 = T2 H4 : ctx L1 * H5 : member (of (E n1) T2) L1 H6 : member (of (E n1) T2) L1 ============================ T2 = T2 ctx_uniq <search.Proof completed.

Abella <Theorem abs_ins_arr : forall L R N U T S, ctx L -> {L |- of (abs R) S} -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}.

============================ forall L R N U T S, ctx L -> {L |- of (abs R) S} -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} abs_ins_arr <induction on 2.

IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} ============================ forall L R N U T S, ctx L -> {L |- of (abs R) S}@ -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} abs_ins_arr <intros.

Variables: L R N U T S IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H2 : {L |- of (abs R) S}@ H3 : {L |- ins* S (arr U T)} H4 : {L |- of N U} ============================ {L |- of (R N) T} abs_ins_arr <case H2.

Subgoal 1: Variables: L R N U T U1 T1 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* (arr T1 U1) (arr U T)} H4 : {L |- of N U} H5 : {L, of n1 T1 |- of (R n1) U1}* ============================ {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H3.

Subgoal 1.1: Variables: L R N U T IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 U |- of (R n1) T}* ============================ {L |- of (R N) T} Subgoal 1.2 is: {L |- of (R N) T} Subgoal 1.3 is: {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <inst H5 with n1 = N.

Subgoal 1.1: Variables: L R N U T IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 U |- of (R n1) T}* H6 : {L, of N U |- of (R N) T}* ============================ {L |- of (R N) T} Subgoal 1.2 is: {L |- of (R N) T} Subgoal 1.3 is: {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <cut H6 with H4.

Subgoal 1.1: Variables: L R N U T IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 U |- of (R n1) T}* H6 : {L, of N U |- of (R N) T}* H7 : {L |- of (R N) T} ============================ {L |- of (R N) T} Subgoal 1.2 is: {L |- of (R N) T} Subgoal 1.3 is: {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <search.

Subgoal 1.2: Variables: L R N U T U1 T1 U2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 T1 |- of (R n1) U1}* H6 : {L |- ins (arr T1 U1) U2} H7 : {L |- ins* U2 (arr U T)} ============================ {L |- of (R N) T} Subgoal 1.3 is: {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H6.

Subgoal 1.2: Variables: L R N U T U1 T1 U2 F IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 T1 |- of (R n1) U1}* H7 : {L |- ins* U2 (arr U T)} H8 : {L, [F] |- ins (arr T1 U1) U2} H9 : member F L ============================ {L |- of (R N) T} Subgoal 1.3 is: {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <apply of_name to _ H9.

Subgoal 1.2: Variables: L R N U T U1 T1 U2 X T2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 T1 |- of (R n1) U1}* H7 : {L |- ins* U2 (arr U T)} H8 : {L, [of X T2] |- ins (arr T1 U1) U2} H9 : member (of X T2) L H10 : name X ============================ {L |- of (R N) T} Subgoal 1.3 is: {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H8.

Subgoal 1.3: Variables: L R N U T U1 T1 F IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 T1 |- of (R n1) U1}* H6 : {L, [F] |- ins* (arr T1 U1) (arr U T)} H7 : member F L ============================ {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <apply of_name to _ H7.

Subgoal 1.3: Variables: L R N U T U1 T1 X T2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L, of n1 T1 |- of (R n1) U1}* H6 : {L, [of X T2] |- ins* (arr T1 U1) (arr U T)} H7 : member (of X T2) L H8 : name X ============================ {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H6.

Subgoal 2: Variables: L R N U T T1 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* (all T1) (arr U T)} H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* ============================ {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H3.

Subgoal 2.1: Variables: L R N U T T1 U1 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H6 : {L |- ins (all T1) U1} H7 : {L |- ins* U1 (arr U T)} ============================ {L |- of (R N) T} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H6.

Subgoal 2.1.1: Variables: L R N U T T1 U2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H7 : {L |- ins* (T1 U2) (arr U T)} ============================ {L |- of (R N) T} Subgoal 2.1.2 is: {L |- of (R N) T} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <inst H5 with n1 = U2.

Subgoal 2.1.1: Variables: L R N U T T1 U2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H7 : {L |- ins* (T1 U2) (arr U T)} H8 : {L |- of (abs R) (T1 U2)}* ============================ {L |- of (R N) T} Subgoal 2.1.2 is: {L |- of (R N) T} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <apply IH to _ H8 H7 H4.

Subgoal 2.1.1: Variables: L R N U T T1 U2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H7 : {L |- ins* (T1 U2) (arr U T)} H8 : {L |- of (abs R) (T1 U2)}* H9 : {L |- of (R N) T} ============================ {L |- of (R N) T} Subgoal 2.1.2 is: {L |- of (R N) T} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <search.

Subgoal 2.1.2: Variables: L R N U T T1 U1 F IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H7 : {L |- ins* U1 (arr U T)} H8 : {L, [F] |- ins (all T1) U1} H9 : member F L ============================ {L |- of (R N) T} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <apply of_name to _ H9.

Subgoal 2.1.2: Variables: L R N U T T1 U1 X T2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H7 : {L |- ins* U1 (arr U T)} H8 : {L, [of X T2] |- ins (all T1) U1} H9 : member (of X T2) L H10 : name X ============================ {L |- of (R N) T} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H8.

Subgoal 2.2: Variables: L R N U T T1 F IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H6 : {L, [F] |- ins* (all T1) (arr U T)} H7 : member F L ============================ {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <apply of_name to _ H7.

Subgoal 2.2: Variables: L R N U T T1 X T2 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H4 : {L |- of N U} H5 : {L |- of (abs R) (T1 n1)}* H6 : {L, [of X T2] |- ins* (all T1) (arr U T)} H7 : member (of X T2) L H8 : name X ============================ {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <case H6.

Subgoal 3: Variables: L R N U T T1 U1 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* (T1 U1) (arr U T)} H4 : {L |- of N U} H5 : {L |- of (abs R) (all T1)}* ============================ {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <assert {L |- ins* (all T1) (arr U T)}.

Subgoal 3: Variables: L R N U T T1 U1 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* (T1 U1) (arr U T)} H4 : {L |- of N U} H5 : {L |- of (abs R) (all T1)}* H6 : {L |- ins* (all T1) (arr U T)} ============================ {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <apply IH to _ H5 H6 H4.

Subgoal 3: Variables: L R N U T T1 U1 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* (T1 U1) (arr U T)} H4 : {L |- of N U} H5 : {L |- of (abs R) (all T1)}* H6 : {L |- ins* (all T1) (arr U T)} H7 : {L |- of (R N) T} ============================ {L |- of (R N) T} Subgoal 4 is: {L |- of (R N) T} abs_ins_arr <search.

Subgoal 4: Variables: L R N U T S F IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* S (arr U T)} H4 : {L |- of N U} H5 : {L, [F] |- of (abs R) S}* H6 : member F L ============================ {L |- of (R N) T} abs_ins_arr <apply of_name to _ H6.

Subgoal 4: Variables: L R N U T S X T1 IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* S (arr U T)} H4 : {L |- of N U} H5 : {L, [of X T1] |- of (abs R) S}* H6 : member (of X T1) L H7 : name X ============================ {L |- of (R N) T} abs_ins_arr <case H5.

Subgoal 4: Variables: L R N U T S IH : forall L R N U T S, ctx L -> {L |- of (abs R) S}* -> {L |- ins* S (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- ins* S (arr U T)} H4 : {L |- of N U} H6 : member (of (abs R) S) L H7 : name (abs R) ============================ {L |- of (R N) T} abs_ins_arr <case H7.Proof completed.

Abella <Theorem abs_arr : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)} -> {L |- of N U} -> {L |- of (R N) T}.

============================ forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)} -> {L |- of N U} -> {L |- of (R N) T} abs_arr <induction on 2.

IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} ============================ forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}@ -> {L |- of N U} -> {L |- of (R N) T} abs_arr <intros.

Variables: L R N U T IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H2 : {L |- of (abs R) (arr U T)}@ H3 : {L |- of N U} ============================ {L |- of (R N) T} abs_arr <case H2.

Subgoal 1: Variables: L R N U T IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H4 : {L, of n1 U |- of (R n1) T}* ============================ {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <inst H4 with n1 = N.

Subgoal 1: Variables: L R N U T IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H4 : {L, of n1 U |- of (R n1) T}* H5 : {L, of N U |- of (R N) T}* ============================ {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <cut H5 with H3.

Subgoal 1: Variables: L R N U T IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H4 : {L, of n1 U |- of (R n1) T}* H5 : {L, of N U |- of (R N) T}* H6 : {L |- of (R N) T} ============================ {L |- of (R N) T} Subgoal 2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <search.

Subgoal 2: Variables: L R N U T T1 U1 IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H4 : T1 U1 = arr U T H5 : {L |- of (abs R) (all T1)}* ============================ {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <case H4.

Subgoal 2.1: Variables: L R N U1 T3 T2 IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N (T2 U1)} H5 : {L |- of (abs R) (all (z1\arr (T2 z1) (T3 z1)))}* ============================ {L |- of (R N) (T3 U1)} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <assert {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))}.

Subgoal 2.1: Variables: L R N U1 T3 T2 IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N (T2 U1)} H5 : {L |- of (abs R) (all (z1\arr (T2 z1) (T3 z1)))}* H6 : {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))} ============================ {L |- of (R N) (T3 U1)} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <apply abs_ins_arr to _ H5 H6 H3.

Subgoal 2.1: Variables: L R N U1 T3 T2 IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N (T2 U1)} H5 : {L |- of (abs R) (all (z1\arr (T2 z1) (T3 z1)))}* H6 : {L |- ins* (all (z1\arr (T2 z1) (T3 z1))) (arr (T2 U1) (T3 U1))} H7 : {L |- of (R N) (T3 U1)} ============================ {L |- of (R N) (T3 U1)} Subgoal 2.2 is: {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <search.

Subgoal 2.2: Variables: L R N U T IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H5 : {L |- of (abs R) (all z1\z1)}* ============================ {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <assert {L |- ins* (all z1\z1) (arr U T)}.

Subgoal 2.2: Variables: L R N U T IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H5 : {L |- of (abs R) (all z1\z1)}* H6 : {L |- ins* (all z1\z1) (arr U T)} ============================ {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <apply abs_ins_arr to _ H5 H6 H3.

Subgoal 2.2: Variables: L R N U T IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H5 : {L |- of (abs R) (all z1\z1)}* H6 : {L |- ins* (all z1\z1) (arr U T)} H7 : {L |- of (R N) T} ============================ {L |- of (R N) T} Subgoal 3 is: {L |- of (R N) T} abs_arr <search.

Subgoal 3: Variables: L R N U T F IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H4 : {L, [F] |- of (abs R) (arr U T)}* H5 : member F L ============================ {L |- of (R N) T} abs_arr <apply of_name to _ H5.

Subgoal 3: Variables: L R N U T X T1 IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx L H3 : {L |- of N U} H4 : {L, [of X T1] |- of (abs R) (arr U T)}* H5 : member (of X T1) L H6 : name X ============================ {L |- of (R N) T} abs_arr <case H6.

Subgoal 3: Variables: L R N U T T1 IH : forall L R N U T, ctx L -> {L |- of (abs R) (arr U T)}* -> {L |- of N U} -> {L |- of (R N) T} H1 : ctx (L n1) H3 : {L n1 |- of (N n1) U} H4 : {L n1, [of n1 T1] |- of (abs (R n1)) (arr U T)}* H5 : member (of n1 T1) (L n1) ============================ {L n1 |- of (R n1 (N n1)) T} abs_arr <case H4.Proof completed.

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

============================ forall L M N T, ctx L -> {L |- of M T} -> {step M N} -> {L |- of N T} step_preserves_of <induction on 2.

IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} ============================ forall L M N T, ctx L -> {L |- of M T}@ -> {step M N} -> {L |- of N T} step_preserves_of <intros.

Variables: L M N T IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H2 : {L |- of M T}@ H3 : {step M N} ============================ {L |- of N T} step_preserves_of <case H2.

Subgoal 1: Variables: L N T U N1 M1 IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step (app M1 N1) N} H4 : {L |- of M1 (arr U T)}* H5 : {L |- of N1 U}* ============================ {L |- of N T} Subgoal 2 is: {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <case H3.

Subgoal 1.1: Variables: L T U N1 M1 M' IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L |- of M1 (arr U T)}* H5 : {L |- of N1 U}* H6 : {step M1 M'} ============================ {L |- of (app M' N1) T} Subgoal 1.2 is: {L |- of (app M1 N') T} Subgoal 1.3 is: {L |- of (R N1) T} Subgoal 2 is: {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <apply IH to _ H4 H6.

Subgoal 1.1: Variables: L T U N1 M1 M' IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L |- of M1 (arr U T)}* H5 : {L |- of N1 U}* H6 : {step M1 M'} H7 : {L |- of M' (arr U T)} ============================ {L |- of (app M' N1) T} Subgoal 1.2 is: {L |- of (app M1 N') T} Subgoal 1.3 is: {L |- of (R N1) T} Subgoal 2 is: {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <search.

Subgoal 1.2: Variables: L T U N1 M1 N' IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L |- of M1 (arr U T)}* H5 : {L |- of N1 U}* H6 : {step N1 N'} ============================ {L |- of (app M1 N') T} Subgoal 1.3 is: {L |- of (R N1) T} Subgoal 2 is: {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <apply IH to _ H5 H6.

Subgoal 1.2: Variables: L T U N1 M1 N' IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L |- of M1 (arr U T)}* H5 : {L |- of N1 U}* H6 : {step N1 N'} H7 : {L |- of N' U} ============================ {L |- of (app M1 N') T} Subgoal 1.3 is: {L |- of (R N1) T} Subgoal 2 is: {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <search.

Subgoal 1.3: Variables: L T U N1 R IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L |- of (abs R) (arr U T)}* H5 : {L |- of N1 U}* ============================ {L |- of (R N1) T} Subgoal 2 is: {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <apply abs_arr to _ H4 H5.

Subgoal 1.3: Variables: L T U N1 R IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L |- of (abs R) (arr U T)}* H5 : {L |- of N1 U}* H6 : {L |- of (R N1) T} ============================ {L |- of (R N1) T} Subgoal 2 is: {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <search.

Subgoal 2: Variables: L N U R T1 IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step (abs R) N} H4 : {L, of n1 T1 |- of (R n1) U}* ============================ {L |- of N (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <case H3.

Subgoal 2: Variables: L U R T1 R' IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L, of n1 T1 |- of (R n1) U}* H5 : {step (R n1) (R' n1)} ============================ {L |- of (abs R') (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <apply IH to _ H4 H5.

Subgoal 2: Variables: L U R T1 R' IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H4 : {L, of n1 T1 |- of (R n1) U}* H5 : {step (R n1) (R' n1)} H6 : {L, of n1 T1 |- of (R' n1) U} ============================ {L |- of (abs R') (arr T1 U)} Subgoal 3 is: {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <search.

Subgoal 3: Variables: L M N T1 IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step M N} H4 : {L |- of M (T1 n1)}* ============================ {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <apply IH to _ H4 H3.

Subgoal 3: Variables: L M N T1 IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step M N} H4 : {L |- of M (T1 n1)}* H5 : {L |- of N (T1 n1)} ============================ {L |- of N (all T1)} Subgoal 4 is: {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <search.

Subgoal 4: Variables: L M N T1 U IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step M N} H4 : {L |- of M (all T1)}* ============================ {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <apply IH to _ H4 H3.

Subgoal 4: Variables: L M N T1 U IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step M N} H4 : {L |- of M (all T1)}* H5 : {L |- of N (all T1)} ============================ {L |- of N (T1 U)} Subgoal 5 is: {L |- of N T} step_preserves_of <search.

Subgoal 5: Variables: L M N T F IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step M N} H4 : {L, [F] |- of M T}* H5 : member F L ============================ {L |- of N T} step_preserves_of <apply of_name to _ H5.

Subgoal 5: Variables: L M N T X T1 IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step M N} H4 : {L, [of X T1] |- of M T}* H5 : member (of X T1) L H6 : name X ============================ {L |- of N T} step_preserves_of <case H4.

Subgoal 5: Variables: L M N T IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H3 : {step M N} H5 : member (of M T) L H6 : name M ============================ {L |- of N T} step_preserves_of <case H3.

Subgoal 5.1: Variables: L T M' M1 N1 IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H5 : member (of (app M1 N1) T) L H6 : name (app M1 N1) H7 : {step M1 M'} ============================ {L |- of (app M' N1) T} Subgoal 5.2 is: {L |- of (app M1 N') T} Subgoal 5.3 is: {L |- of (abs R') T} Subgoal 5.4 is: {L |- of (R N1) T} step_preserves_of <case H6.

Subgoal 5.2: Variables: L T N' N1 M1 IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H5 : member (of (app M1 N1) T) L H6 : name (app M1 N1) H7 : {step N1 N'} ============================ {L |- of (app M1 N') T} Subgoal 5.3 is: {L |- of (abs R') T} Subgoal 5.4 is: {L |- of (R N1) T} step_preserves_of <case H6.

Subgoal 5.3: Variables: L T R' R IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H5 : member (of (abs R) T) L H6 : name (abs R) H7 : {step (R n1) (R' n1)} ============================ {L |- of (abs R') T} Subgoal 5.4 is: {L |- of (R N1) T} step_preserves_of <case H6.

Subgoal 5.4: Variables: L T N1 R IH : forall L M N T, ctx L -> {L |- of M T}* -> {step M N} -> {L |- of N T} H1 : ctx L H5 : member (of (app (abs R) N1) T) L H6 : name (app (abs R) N1) ============================ {L |- of (R N1) T} step_preserves_of <case H6.Proof completed.

Abella <