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 <