Welcome to Abella 2.0.5-dev.

Abella <Specification "pcf".Reading specification "pcf".

Abella <Theorem subject_reduction : forall E V T, {eval E V} -> {of E T} -> {of V T}.

============================ forall E V T, {eval E V} -> {of E T} -> {of V T} subject_reduction <induction on 1.

IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} ============================ forall E V T, {eval E V}@ -> {of E T} -> {of V T} subject_reduction <intros.

Variables: E V T IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H1 : {eval E V}@ H2 : {of E T} ============================ {of V T} subject_reduction <case H1.

Subgoal 1: Variables: T IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of zero T} ============================ {of zero T} Subgoal 2 is: {of tt T} Subgoal 3 is: {of ff T} Subgoal 4 is: {of (succ V1) T} Subgoal 5 is: {of zero T} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 2: Variables: T IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of tt T} ============================ {of tt T} Subgoal 3 is: {of ff T} Subgoal 4 is: {of (succ V1) T} Subgoal 5 is: {of zero T} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 3: Variables: T IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of ff T} ============================ {of ff T} Subgoal 4 is: {of (succ V1) T} Subgoal 5 is: {of zero T} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 4: Variables: T V1 M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (succ M) T} H3 : {eval M V1}* ============================ {of (succ V1) T} Subgoal 5 is: {of zero T} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 4: Variables: V1 M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M V1}* H4 : {of M num} ============================ {of (succ V1) num} Subgoal 5 is: {of zero T} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <apply IH to H3 H4.

Subgoal 4: Variables: V1 M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M V1}* H4 : {of M num} H5 : {of V1 num} ============================ {of (succ V1) num} Subgoal 5 is: {of zero T} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 5: Variables: T M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (pred M) T} H3 : {eval M zero}* ============================ {of zero T} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 5: Variables: M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M zero}* H4 : {of M num} ============================ {of zero num} Subgoal 6 is: {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 6: Variables: V T M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (pred M) T} H3 : {eval M (succ V)}* ============================ {of V T} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 6: Variables: V M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (succ V)}* H4 : {of M num} ============================ {of V num} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <apply IH to H3 H4.

Subgoal 6: Variables: V M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (succ V)}* H4 : {of M num} H5 : {of (succ V) num} ============================ {of V num} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H5.

Subgoal 6: Variables: V M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (succ V)}* H4 : {of M num} H6 : {of V num} ============================ {of V num} Subgoal 7 is: {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 7: Variables: T M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (is_zero M) T} H3 : {eval M zero}* ============================ {of tt T} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 7: Variables: M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M zero}* H4 : {of M num} ============================ {of tt bool} Subgoal 8 is: {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 8: Variables: T V1 M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (is_zero M) T} H3 : {eval M (succ V1)}* ============================ {of ff T} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 8: Variables: V1 M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (succ V1)}* H4 : {of M num} ============================ {of ff bool} Subgoal 9 is: {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 9: Variables: V T N1 M N2 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (if M N1 N2) T} H3 : {eval M tt}* H4 : {eval N1 V}* ============================ {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 9: Variables: V T N1 M N2 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M tt}* H4 : {eval N1 V}* H5 : {of M bool} H6 : {of N1 T} H7 : {of N2 T} ============================ {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <apply IH to H4 H6.

Subgoal 9: Variables: V T N1 M N2 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M tt}* H4 : {eval N1 V}* H5 : {of M bool} H6 : {of N1 T} H7 : {of N2 T} H8 : {of V T} ============================ {of V T} Subgoal 10 is: {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 10: Variables: V T N2 M N1 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (if M N1 N2) T} H3 : {eval M ff}* H4 : {eval N2 V}* ============================ {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 10: Variables: V T N2 M N1 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M ff}* H4 : {eval N2 V}* H5 : {of M bool} H6 : {of N1 T} H7 : {of N2 T} ============================ {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <apply IH to H4 H7.

Subgoal 10: Variables: V T N2 M N1 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M ff}* H4 : {eval N2 V}* H5 : {of M bool} H6 : {of N1 T} H7 : {of N2 T} H8 : {of V T} ============================ {of V T} Subgoal 11 is: {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 11: Variables: T R T1 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (abs T1 R) T} ============================ {of (abs T1 R) T} Subgoal 12 is: {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 12: Variables: V T N R T1 M IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (app M N) T} H3 : {eval M (abs T1 R)}* H4 : {eval (R N) V}* ============================ {of V T} Subgoal 13 is: {of V T} subject_reduction <case H2.

Subgoal 12: Variables: V T N R T1 M U IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (abs T1 R)}* H4 : {eval (R N) V}* H5 : {of M (arr U T)} H6 : {of N U} ============================ {of V T} Subgoal 13 is: {of V T} subject_reduction <apply IH to H3 H5.

Subgoal 12: Variables: V T N R T1 M U IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (abs T1 R)}* H4 : {eval (R N) V}* H5 : {of M (arr U T)} H6 : {of N U} H7 : {of (abs T1 R) (arr U T)} ============================ {of V T} Subgoal 13 is: {of V T} subject_reduction <case H7.

Subgoal 12: Variables: V T N R M U IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (abs U R)}* H4 : {eval (R N) V}* H5 : {of M (arr U T)} H6 : {of N U} H8 : {of n1 U |- of (R n1) T} ============================ {of V T} Subgoal 13 is: {of V T} subject_reduction <inst H8 with n1 = N.

Subgoal 12: Variables: V T N R M U IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (abs U R)}* H4 : {eval (R N) V}* H5 : {of M (arr U T)} H6 : {of N U} H8 : {of n1 U |- of (R n1) T} H9 : {of N U |- of (R N) T} ============================ {of V T} Subgoal 13 is: {of V T} subject_reduction <cut H9 with H6.

Subgoal 12: Variables: V T N R M U IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (abs U R)}* H4 : {eval (R N) V}* H5 : {of M (arr U T)} H6 : {of N U} H8 : {of n1 U |- of (R n1) T} H9 : {of N U |- of (R N) T} H10 : {of (R N) T} ============================ {of V T} Subgoal 13 is: {of V T} subject_reduction <apply IH to H4 H10.

Subgoal 12: Variables: V T N R M U IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H3 : {eval M (abs U R)}* H4 : {eval (R N) V}* H5 : {of M (arr U T)} H6 : {of N U} H8 : {of n1 U |- of (R n1) T} H9 : {of N U |- of (R N) T} H10 : {of (R N) T} H11 : {of V T} ============================ {of V T} Subgoal 13 is: {of V T} subject_reduction <search.

Subgoal 13: Variables: V T R T1 IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (rec T1 R) T} H3 : {eval (R (rec T1 R)) V}* ============================ {of V T} subject_reduction <case H2 (keep).

Subgoal 13: Variables: V T R IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (rec T R) T} H3 : {eval (R (rec T R)) V}* H4 : {of n1 T |- of (R n1) T} ============================ {of V T} subject_reduction <inst H4 with n1 = rec T R.

Subgoal 13: Variables: V T R IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (rec T R) T} H3 : {eval (R (rec T R)) V}* H4 : {of n1 T |- of (R n1) T} H5 : {of (rec T R) T |- of (R (rec T R)) T} ============================ {of V T} subject_reduction <cut H5 with H2.

Subgoal 13: Variables: V T R IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (rec T R) T} H3 : {eval (R (rec T R)) V}* H4 : {of n1 T |- of (R n1) T} H5 : {of (rec T R) T |- of (R (rec T R)) T} H6 : {of (R (rec T R)) T} ============================ {of V T} subject_reduction <apply IH to H3 H6.

Subgoal 13: Variables: V T R IH : forall E V T, {eval E V}* -> {of E T} -> {of V T} H2 : {of (rec T R) T} H3 : {eval (R (rec T R)) V}* H4 : {of n1 T |- of (R n1) T} H5 : {of (rec T R) T |- of (R (rec T R)) T} H6 : {of (R (rec T R)) T} H7 : {of V T} ============================ {of V T} subject_reduction <search.Proof completed.

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 A :: L) := 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).

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

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

Variables: E L IH : forall E L, ctx L * -> member E L -> (exists X A, E = of X A /\ name X) H1 : ctx L @ H2 : member E L ============================ exists X A, E = of X A /\ name X 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) H2 : member E nil ============================ exists X A, E = of X A /\ name X Subgoal 2 is: exists X A, E n1 = of X A /\ name X 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) H2 : member (E n1) (of n1 A :: L1) H3 : ctx L1 * ============================ exists X A, E n1 = of X A /\ name X 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) H3 : ctx L1 * ============================ exists X A1, of n1 A = of X A1 /\ name X Subgoal 2.2 is: exists X A, E n1 = of X A /\ name X 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) H3 : ctx L1 * H4 : member (E n1) L1 ============================ exists X A, E n1 = of X A /\ name X ctx_member <apply IH to H3 H4.

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) H3 : ctx L1 * H4 : member (of (X n1) (A1 n1)) L1 H5 : name (X n1) ============================ exists X1 A, of (X n1) (A1 n1) = of X1 A /\ name X1 ctx_member <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 n1 = T2 n1 ctx_uniq <case H2.

Subgoal 2: Variables: E T1 T2 L1 A 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 n1)) (of n1 A :: L1) H3 : member (of (E n1) (T2 n1)) (of n1 A :: L1) H4 : ctx L1 * ============================ T1 n1 = T2 n1 ctx_uniq <case H2.

Subgoal 2.1: Variables: T2 L1 A 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 n1)) (of n1 A :: L1) H4 : ctx L1 * ============================ A = T2 n1 Subgoal 2.2 is: T1 n1 = T2 n1 ctx_uniq <case H3.

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

Subgoal 2.1.2: Variables: T2 L1 A 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 n1)) L1 ============================ A = T2 n1 Subgoal 2.2 is: T1 n1 = T2 n1 ctx_uniq <apply member_prune to H5.

Subgoal 2.2: Variables: E T1 T2 L1 A 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 n1)) (of n1 A :: L1) H4 : ctx L1 * H5 : member (of (E n1) (T1 n1)) L1 ============================ T1 n1 = T2 n1 ctx_uniq <case H3.

Subgoal 2.2.1: Variables: T1 L1 A 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 n1)) L1 ============================ T1 n1 = A Subgoal 2.2.2 is: T1 n1 = T2 n1 ctx_uniq <apply member_prune to H5.

Subgoal 2.2.2: Variables: E T1 T2 L1 A 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 n1)) L1 H6 : member (of (E n1) (T2 n1)) L1 ============================ T1 n1 = T2 n1 ctx_uniq <apply IH to H4 H5 H6.

Subgoal 2.2.2: Variables: E T2 L1 A 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 n1)) L1 H6 : member (of (E n1) (T2 n1)) L1 ============================ T2 n1 = T2 n1 ctx_uniq <search.Proof completed.

Abella <Theorem type_uniq : forall L E T1 T2, ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.

============================ forall L E T1 T2, ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2 type_uniq <induction on 2.

IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 ============================ forall L E T1 T2, ctx L -> {L |- of E T1}@ -> {L |- of E T2} -> T1 = T2 type_uniq <intros.

Variables: L E T1 T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H2 : {L |- of E T1}@ H3 : {L |- of E T2} ============================ T1 = T2 type_uniq <case H2.

Subgoal 1: Variables: L T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of zero T2} ============================ num = T2 Subgoal 2 is: bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 1.1: Variables: L IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L ============================ num = num Subgoal 1.2 is: num = T2 Subgoal 2 is: bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 1.2: Variables: L T2 F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, [F] |- of zero T2} H5 : member F L ============================ num = T2 Subgoal 2 is: bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H5.

Subgoal 1.2: Variables: L T2 X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, [of X A] |- of zero T2} H5 : member (of X A) L H6 : name X ============================ num = T2 Subgoal 2 is: bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H4.

Subgoal 1.2: Variables: L T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H5 : member (of zero T2) L H6 : name zero ============================ num = T2 Subgoal 2 is: bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H6.

Subgoal 2: Variables: L T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of tt T2} ============================ bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 2.1: Variables: L IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L ============================ bool = bool Subgoal 2.2 is: bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 2.2: Variables: L T2 F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, [F] |- of tt T2} H5 : member F L ============================ bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H5.

Subgoal 2.2: Variables: L T2 X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, [of X A] |- of tt T2} H5 : member (of X A) L H6 : name X ============================ bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H4.

Subgoal 2.2: Variables: L T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H5 : member (of tt T2) L H6 : name tt ============================ bool = T2 Subgoal 3 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H6.

Subgoal 3: Variables: L T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of ff T2} ============================ bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 3.1: Variables: L IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L ============================ bool = bool Subgoal 3.2 is: bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 3.2: Variables: L T2 F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, [F] |- of ff T2} H5 : member F L ============================ bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H5.

Subgoal 3.2: Variables: L T2 X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, [of X A] |- of ff T2} H5 : member (of X A) L H6 : name X ============================ bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H4.

Subgoal 3.2: Variables: L T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H5 : member (of ff T2) L H6 : name ff ============================ bool = T2 Subgoal 4 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H6.

Subgoal 4: Variables: L T2 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (succ M) T2} H4 : {L |- of M num}* ============================ num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 4.1: Variables: L M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L |- of M num} ============================ num = num Subgoal 4.2 is: num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 4.2: Variables: L T2 M F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L, [F] |- of (succ M) T2} H6 : member F L ============================ num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H6.

Subgoal 4.2: Variables: L T2 M X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L, [of X A] |- of (succ M) T2} H6 : member (of X A) L H7 : name X ============================ num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H5.

Subgoal 4.2: Variables: L T2 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H6 : member (of (succ M) T2) L H7 : name (succ M) ============================ num = T2 Subgoal 5 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H7.

Subgoal 5: Variables: L T2 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (pred M) T2} H4 : {L |- of M num}* ============================ num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 5.1: Variables: L M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L |- of M num} ============================ num = num Subgoal 5.2 is: num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 5.2: Variables: L T2 M F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L, [F] |- of (pred M) T2} H6 : member F L ============================ num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H6.

Subgoal 5.2: Variables: L T2 M X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L, [of X A] |- of (pred M) T2} H6 : member (of X A) L H7 : name X ============================ num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H5.

Subgoal 5.2: Variables: L T2 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H6 : member (of (pred M) T2) L H7 : name (pred M) ============================ num = T2 Subgoal 6 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H7.

Subgoal 6: Variables: L T2 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (is_zero M) T2} H4 : {L |- of M num}* ============================ bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 6.1: Variables: L M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L |- of M num} ============================ bool = bool Subgoal 6.2 is: bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 6.2: Variables: L T2 M F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L, [F] |- of (is_zero M) T2} H6 : member F L ============================ bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H6.

Subgoal 6.2: Variables: L T2 M X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H5 : {L, [of X A] |- of (is_zero M) T2} H6 : member (of X A) L H7 : name X ============================ bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H5.

Subgoal 6.2: Variables: L T2 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M num}* H6 : member (of (is_zero M) T2) L H7 : name (is_zero M) ============================ bool = T2 Subgoal 7 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H7.

Subgoal 7: Variables: L T1 T2 N2 N1 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (if M N1 N2) T2} H4 : {L |- of M bool}* H5 : {L |- of N1 T1}* H6 : {L |- of N2 T1}* ============================ T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 7.1: Variables: L T1 T2 N2 N1 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M bool}* H5 : {L |- of N1 T1}* H6 : {L |- of N2 T1}* H7 : {L |- of M bool} H8 : {L |- of N1 T2} H9 : {L |- of N2 T2} ============================ T1 = T2 Subgoal 7.2 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply IH to H1 H5 H8.

Subgoal 7.1: Variables: L T2 N2 N1 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M bool}* H5 : {L |- of N1 T2}* H6 : {L |- of N2 T2}* H7 : {L |- of M bool} H8 : {L |- of N1 T2} H9 : {L |- of N2 T2} ============================ T2 = T2 Subgoal 7.2 is: T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 7.2: Variables: L T1 T2 N2 N1 M F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M bool}* H5 : {L |- of N1 T1}* H6 : {L |- of N2 T1}* H7 : {L, [F] |- of (if M N1 N2) T2} H8 : member F L ============================ T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H8.

Subgoal 7.2: Variables: L T1 T2 N2 N1 M X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M bool}* H5 : {L |- of N1 T1}* H6 : {L |- of N2 T1}* H7 : {L, [of X A] |- of (if M N1 N2) T2} H8 : member (of X A) L H9 : name X ============================ T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H7.

Subgoal 7.2: Variables: L T1 T2 N2 N1 M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M bool}* H5 : {L |- of N1 T1}* H6 : {L |- of N2 T1}* H8 : member (of (if M N1 N2) T2) L H9 : name (if M N1 N2) ============================ T1 = T2 Subgoal 8 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H9.

Subgoal 8: Variables: L T2 U R T IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (abs T R) T2} H4 : {L, of n1 T |- of (R n1) U}* ============================ arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 8.1: Variables: L U R T U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H5 : {L, of n1 T |- of (R n1) U1} ============================ arr T U = arr T U1 Subgoal 8.2 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply IH to _ H4 H5.

Subgoal 8.1: Variables: L R T U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U1}* H5 : {L, of n1 T |- of (R n1) U1} ============================ arr T U1 = arr T U1 Subgoal 8.2 is: arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 8.2: Variables: L T2 U R T F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H5 : {L, [F] |- of (abs T R) T2} H6 : member F L ============================ arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H6.

Subgoal 8.2: Variables: L T2 U R T X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H5 : {L, [of X A] |- of (abs T R) T2} H6 : member (of X A) L H7 : name X ============================ arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H5.

Subgoal 8.2: Variables: L T2 U R T IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T |- of (R n1) U}* H6 : member (of (abs T R) T2) L H7 : name (abs T R) ============================ arr T U = T2 Subgoal 9 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H7.

Subgoal 9: Variables: L T1 T2 U N M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (app M N) T2} H4 : {L |- of M (arr U T1)}* H5 : {L |- of N U}* ============================ T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 9.1: Variables: L T1 T2 U N M U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arr U T1)}* H5 : {L |- of N U}* H6 : {L |- of M (arr U1 T2)} H7 : {L |- of N U1} ============================ T1 = T2 Subgoal 9.2 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply IH to H1 H4 H6.

Subgoal 9.1: Variables: L T2 N M U1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arr U1 T2)}* H5 : {L |- of N U1}* H6 : {L |- of M (arr U1 T2)} H7 : {L |- of N U1} ============================ T2 = T2 Subgoal 9.2 is: T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 9.2: Variables: L T1 T2 U N M F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arr U T1)}* H5 : {L |- of N U}* H6 : {L, [F] |- of (app M N) T2} H7 : member F L ============================ T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H7.

Subgoal 9.2: Variables: L T1 T2 U N M X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arr U T1)}* H5 : {L |- of N U}* H6 : {L, [of X A] |- of (app M N) T2} H7 : member (of X A) L H8 : name X ============================ T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H6.

Subgoal 9.2: Variables: L T1 T2 U N M IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L |- of M (arr U T1)}* H5 : {L |- of N U}* H7 : member (of (app M N) T2) L H8 : name (app M N) ============================ T1 = T2 Subgoal 10 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H8.

Subgoal 10: Variables: L T1 T2 R IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of (rec T1 R) T2} H4 : {L, of n1 T1 |- of (R n1) T1}* ============================ T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H3.

Subgoal 10.1: Variables: L T2 R IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T2 |- of (R n1) T2}* H5 : {L, of n1 T2 |- of (R n1) T2} ============================ T2 = T2 Subgoal 10.2 is: T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <search.

Subgoal 10.2: Variables: L T1 T2 R F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T1 |- of (R n1) T1}* H5 : {L, [F] |- of (rec T1 R) T2} H6 : member F L ============================ T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <apply ctx_member to H1 H6.

Subgoal 10.2: Variables: L T1 T2 R X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T1 |- of (R n1) T1}* H5 : {L, [of X A] |- of (rec T1 R) T2} H6 : member (of X A) L H7 : name X ============================ T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H5.

Subgoal 10.2: Variables: L T1 T2 R IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H4 : {L, of n1 T1 |- of (R n1) T1}* H6 : member (of (rec T1 R) T2) L H7 : name (rec T1 R) ============================ T1 = T2 Subgoal 11 is: T1 = T2 type_uniq <case H7.

Subgoal 11: Variables: L E T1 T2 F IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of E T2} H4 : {L, [F] |- of E T1}* H5 : member F L ============================ T1 = T2 type_uniq <apply ctx_member to H1 H5.

Subgoal 11: Variables: L E T1 T2 X A IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of E T2} H4 : {L, [of X A] |- of E T1}* H5 : member (of X A) L H6 : name X ============================ T1 = T2 type_uniq <case H4.

Subgoal 11: Variables: L E T1 T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx L H3 : {L |- of E T2} H5 : member (of E T1) L H6 : name E ============================ T1 = T2 type_uniq <case H6.

Subgoal 11: Variables: L T1 T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H3 : {L n1 |- of n1 (T2 n1)} H5 : member (of n1 (T1 n1)) (L n1) ============================ T1 n1 = T2 n1 type_uniq <case H3.

Subgoal 11: Variables: L T1 T2 F1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 (T1 n1)) (L n1) H7 : {L n1, [F1 n1] |- of n1 (T2 n1)} H8 : member (F1 n1) (L n1) ============================ T1 n1 = T2 n1 type_uniq <apply ctx_member to H1 H8.

Subgoal 11: Variables: L T1 T2 X1 A1 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 (T1 n1)) (L n1) H7 : {L n1, [of (X1 n1) (A1 n1)] |- of n1 (T2 n1)} H8 : member (of (X1 n1) (A1 n1)) (L n1) H9 : name (X1 n1) ============================ T1 n1 = T2 n1 type_uniq <case H7.

Subgoal 11: Variables: L T1 T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 (T1 n1)) (L n1) H8 : member (of n1 (T2 n1)) (L n1) H9 : name n1 ============================ T1 n1 = T2 n1 type_uniq <apply ctx_uniq to H1 H5 H8.

Subgoal 11: Variables: L T2 IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2 H1 : ctx (L n1) H5 : member (of n1 (T2 n1)) (L n1) H8 : member (of n1 (T2 n1)) (L n1) H9 : name n1 ============================ T2 n1 = T2 n1 type_uniq <search.Proof completed.

Abella <Set search_depth 30.

Abella <Query Add = rec (arr num (arr num num)) (add\abs num (x\abs num (y\if (is_zero x) y (succ (app (app add (pred x)) y))))) /\ Two = succ (succ zero) /\ Three = succ (succ (succ zero)) /\ {eval (app (app Add Two) Three) V}.Found solution: Add = rec (arr num (arr num num)) (add\abs num (x\abs num (y\if (is_zero x) y (succ (app (app add (pred x)) y))))) Two = succ (succ zero) Three = succ (succ (succ zero)) V = succ (succ (succ (succ (succ zero)))) No more solutions.

Abella <