Welcome to Abella 2.0.5-dev.
Abella < Specification "type-uniq".
Reading specification "type-uniq".

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

Abella < Define fresh : tm -> o -> prop by 
nabla x, fresh x E.

Abella < Define freshlist : tm -> olist -> prop by 
nabla x, freshlist x E.

Abella < Theorem member_fresh : 
forall X L E, member E L -> freshlist X L -> fresh X E.


============================
 forall X L E, member E L -> freshlist X L -> fresh X E

member_fresh < induction on 1.

IH : forall X L E, member E L * -> freshlist X L -> fresh X E
============================
 forall X L E, member E L @ -> freshlist X L -> fresh X E

member_fresh < intros.

Variables: X L E
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
H1 : member E L @
H2 : freshlist X L
============================
 fresh X E

member_fresh < case H1.
Subgoal 1:

Variables: X E L1
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
H2 : freshlist X (E :: L1)
============================
 fresh X E

Subgoal 2 is:
 fresh X E

member_fresh < case H2.
Subgoal 1:

Variables: E3 E2
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
============================
 fresh n1 E2

Subgoal 2 is:
 fresh X E

member_fresh < search.
Subgoal 2:

Variables: X E L1 B
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
H2 : freshlist X (B :: L1)
H3 : member E L1 *
============================
 fresh X E

member_fresh < assert freshlist X L1.
Subgoal 2.1:

Variables: X E L1 B
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
H2 : freshlist X (B :: L1)
H3 : member E L1 *
============================
 freshlist X L1

Subgoal 2 is:
 fresh X E

member_fresh < case H2.
Subgoal 2.1:

Variables: E E3 E2
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
H3 : member (E n1) E3 *
============================
 freshlist n1 E3

Subgoal 2 is:
 fresh X E

member_fresh < search.
Subgoal 2:

Variables: X E L1 B
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
H2 : freshlist X (B :: L1)
H3 : member E L1 *
H4 : freshlist X L1
============================
 fresh X E

member_fresh < apply IH to H3 H4.
Subgoal 2:

Variables: X E L1 B
IH : forall X L E, member E L * -> freshlist X L -> fresh X E
H2 : freshlist X (B :: L1)
H3 : member E L1 *
H4 : freshlist X L1
H5 : fresh X E
============================
 fresh X E

member_fresh < search.
Proof completed.
Abella < Define ctx : olist -> prop by 
ctx nil;
ctx (of X T :: L) := freshlist X L /\ ctx L.

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 = of X T /\ name X

of_name < case H2.
Subgoal 2:

Variables: E L1 T X
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H2 : member E (of X T :: L1)
H3 : freshlist X L1
H4 : ctx L1 *
============================
 exists X T, E = of X T /\ name X

of_name < case H3.
Subgoal 2:

Variables: E T E1
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 n1) :: E1)
H4 : ctx E1 *
============================
 exists X T, E n1 = of X T /\ name X

of_name < case H2.
Subgoal 2.1:

Variables: T E1
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H4 : ctx E1 *
============================
 exists X T1, of n1 (T n1) = 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 T E1
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H4 : ctx E1 *
H5 : member (E n1) E1
============================
 exists X T, E n1 = of X T /\ name X

of_name < apply IH to H4 H5.
Subgoal 2.2:

Variables: T E1 X1 T1
IH : forall L E, ctx L * -> member E L -> (exists X T, E = of X T /\ name X)
H4 : ctx E1 *
H5 : member (of (X1 n1) (T1 n1)) E1
H6 : name (X1 n1)
============================
 exists X T, of (X1 n1) (T1 n1) = of X T /\ name X

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 X
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) (of X T :: L1)
H3 : member (of E T2) (of X T :: L1)
H4 : freshlist X L1
H5 : ctx L1 *
============================
 T1 = T2

ctx_uniq < case H2.
Subgoal 2.1:

Variables: T2 L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H3 : member (of X T2) (of X T :: L1)
H4 : freshlist X L1
H5 : ctx L1 *
============================
 T = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < case H3.
Subgoal 2.1.1:

Variables: L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : freshlist X L1
H5 : 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 X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : freshlist X L1
H5 : ctx L1 *
H6 : member (of X T2) L1
============================
 T = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < apply member_fresh to H6 H4.
Subgoal 2.1.2:

Variables: T2 L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : freshlist X L1
H5 : ctx L1 *
H6 : member (of X T2) L1
H7 : fresh X (of X T2)
============================
 T = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < case H7.
Subgoal 2.2:

Variables: E T1 T2 L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H3 : member (of E T2) (of X T :: L1)
H4 : freshlist X L1
H5 : ctx L1 *
H6 : member (of E T1) L1
============================
 T1 = T2

ctx_uniq < case H3.
Subgoal 2.2.1:

Variables: T1 L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : freshlist X L1
H5 : ctx L1 *
H6 : member (of X T1) L1
============================
 T1 = T

Subgoal 2.2.2 is:
 T1 = T2

ctx_uniq < apply member_fresh to H6 H4.
Subgoal 2.2.1:

Variables: T1 L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : freshlist X L1
H5 : ctx L1 *
H6 : member (of X T1) L1
H7 : fresh X (of X T1)
============================
 T1 = T

Subgoal 2.2.2 is:
 T1 = T2

ctx_uniq < case H7.
Subgoal 2.2.2:

Variables: E T1 T2 L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : freshlist X L1
H5 : ctx L1 *
H6 : member (of E T1) L1
H7 : member (of E T2) L1
============================
 T1 = T2

ctx_uniq < apply IH to H5 H6 H7.
Subgoal 2.2.2:

Variables: E T2 L1 T X
IH : forall L E T1 T2, ctx L * -> member (of E T1) L -> member (of E T2) L ->
       T1 =
     T2
H4 : freshlist X L1
H5 : ctx L1 *
H6 : member (of E T2) L1
H7 : member (of E T2) L1
============================
 T2 = T2

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 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}*
============================
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < case H3.
Subgoal 1.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}
============================
 arrow T U = arrow T U1

Subgoal 1.2 is:
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < apply IH to _ H4 H5.
Subgoal 1.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}
============================
 arrow T U1 = arrow T U1

Subgoal 1.2 is:
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < search.
Subgoal 1.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
============================
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < apply of_name to H1 H6.
Subgoal 1.2:

Variables: L T2 U R T X T3
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 T3] |- of (abs T R) T2}
H6 : member (of X T3) L
H7 : name X
============================
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < case H7.
Subgoal 1.2:

Variables: L T2 U R T T3
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx (L n2)
H4 : {L n2, of n1 (T n2) |- of (R n2 n1) (U n2)}*
H5 : {L n2, [of n2 (T3 n2)] |- of (abs (T n2) (R n2)) (T2 n2)}
H6 : member (of n2 (T3 n2)) (L n2)
============================
 arrow (T n2) (U n2) = T2 n2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < case H5.
Subgoal 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
H3 : {L |- of (app M N) T2}
H4 : {L |- of M (arrow U T1)}*
H5 : {L |- of N U}*
============================
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < case H3.
Subgoal 2.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 (arrow U T1)}*
H5 : {L |- of N U}*
H6 : {L |- of M (arrow U1 T2)}
H7 : {L |- of N U1}
============================
 T1 = T2

Subgoal 2.2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < apply IH to H1 H4 H6.
Subgoal 2.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 (arrow U1 T2)}*
H5 : {L |- of N U1}*
H6 : {L |- of M (arrow U1 T2)}
H7 : {L |- of N U1}
============================
 T2 = T2

Subgoal 2.2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < search.
Subgoal 2.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 (arrow U T1)}*
H5 : {L |- of N U}*
H6 : {L, [F] |- of (app M N) T2}
H7 : member F L
============================
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < apply of_name to H1 H7.
Subgoal 2.2:

Variables: L T1 T2 U N M X 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 M (arrow U T1)}*
H5 : {L |- of N U}*
H6 : {L, [of X T] |- of (app M N) T2}
H7 : member (of X T) L
H8 : name X
============================
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq < case H8.
Subgoal 2.2:

Variables: L T1 T2 U N M T
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx (L n1)
H4 : {L n1 |- of (M n1) (arrow (U n1) (T1 n1))}*
H5 : {L n1 |- of (N n1) (U n1)}*
H6 : {L n1, [of n1 (T n1)] |- of (app (M n1) (N n1)) (T2 n1)}
H7 : member (of n1 (T n1)) (L n1)
============================
 T1 n1 = T2 n1

Subgoal 3 is:
 T1 = T2

type_uniq < case H6.
Subgoal 3:

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 of_name to H1 H5.
Subgoal 3:

Variables: L E T1 T2 X 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 E T2}
H4 : {L, [of X T] |- of E T1}*
H5 : member (of X T) L
H6 : name X
============================
 T1 = T2

type_uniq < case H6.
Subgoal 3:

Variables: L E T1 T2 T
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 (E n1) (T2 n1)}
H4 : {L n1, [of n1 (T n1)] |- of (E n1) (T1 n1)}*
H5 : member (of n1 (T n1)) (L n1)
============================
 T1 n1 = T2 n1

type_uniq < case H3.
Subgoal 3.1:

Variables: L T1 T U R T3
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx (L n1)
H4 : {L n1, [of n1 (T n1)] |- of (abs (T3 n1) (R n1)) (T1 n1)}*
H5 : member (of n1 (T n1)) (L n1)
H7 : {L n1, of n2 (T3 n1) |- of (R n1 n2) (U n1)}
============================
 T1 n1 = arrow (T3 n1) (U n1)

Subgoal 3.2 is:
 T1 n1 = T2 n1

Subgoal 3.3 is:
 T1 n1 = T2 n1

type_uniq < case H4.
Subgoal 3.2:

Variables: L T1 T2 T U N M
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx (L n1)
H4 : {L n1, [of n1 (T n1)] |- of (app (M n1) (N n1)) (T1 n1)}*
H5 : member (of n1 (T n1)) (L n1)
H7 : {L n1 |- of (M n1) (arrow (U n1) (T2 n1))}
H8 : {L n1 |- of (N n1) (U n1)}
============================
 T1 n1 = T2 n1

Subgoal 3.3 is:
 T1 n1 = T2 n1

type_uniq < case H4.
Subgoal 3.3:

Variables: L E T1 T2 T F1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx (L n1)
H4 : {L n1, [of n1 (T n1)] |- of (E n1) (T1 n1)}*
H5 : member (of n1 (T n1)) (L n1)
H7 : {L n1, [F1 n1] |- of (E n1) (T2 n1)}
H8 : member (F1 n1) (L n1)
============================
 T1 n1 = T2 n1

type_uniq < apply of_name to H1 H8.
Subgoal 3.3:

Variables: L E T1 T2 T X1 T3
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx (L n1)
H4 : {L n1, [of n1 (T n1)] |- of (E n1) (T1 n1)}*
H5 : member (of n1 (T n1)) (L n1)
H7 : {L n1, [of (X1 n1) (T3 n1)] |- of (E n1) (T2 n1)}
H8 : member (of (X1 n1) (T3 n1)) (L n1)
H9 : name (X1 n1)
============================
 T1 n1 = T2 n1

type_uniq < case H7.
Subgoal 3.3:

Variables: L E T1 T2 T
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx (L n1)
H4 : {L n1, [of n1 (T n1)] |- of (E n1) (T1 n1)}*
H5 : member (of n1 (T n1)) (L n1)
H8 : member (of (E n1) (T2 n1)) (L n1)
H9 : name (E n1)
============================
 T1 n1 = T2 n1

type_uniq < case H4.
Subgoal 3.3:

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 3.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 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 <