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 < Theorem member_nominal_absurd : 
forall L T, nabla x, member (of x T) L -> false.


============================
 forall L T, nabla x, member (of x T) L -> false

member_nominal_absurd < induction on 1.

IH : forall L T, nabla x, member (of x T) L * -> false
============================
 forall L T, nabla x, member (of x T) L @ -> false

member_nominal_absurd < intros.

Variables: L T
IH : forall L T, nabla x, member (of x T) L * -> false
H1 : member (of n1 T) L @
============================
 false

member_nominal_absurd < case H1.

Variables: T L3 L2
IH : forall L T, nabla x, member (of x T) L * -> false
H2 : member (of n1 T) L3 *
============================
 false

member_nominal_absurd < apply IH to H2.
Proof completed.
Abella < Close tm, ty.

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

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

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 H2.
Subgoal 1:

Variables: E T1 T2 L1
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H1 : ctx (of E T1 :: L1)
H3 : member (of E T2) (of E T1 :: L1)
============================
 T1 = T2

Subgoal 2 is:
 T1 = T2

ctx_uniq < case H3.
Subgoal 1.1:

Variables: E T1 L1
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H1 : ctx (of E T1 :: L1)
============================
 T1 = T1

Subgoal 1.2 is:
 T1 = T2

Subgoal 2 is:
 T1 = T2

ctx_uniq < search.
Subgoal 1.2:

Variables: E T1 T2 L1
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H1 : ctx (of E T1 :: L1)
H4 : member (of E T2) L1
============================
 T1 = T2

Subgoal 2 is:
 T1 = T2

ctx_uniq < case H1.
Subgoal 1.2:

Variables: T1 T2 L2
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H4 : member (of n1 T2) L2
H5 : ctx L2
============================
 T1 = T2

Subgoal 2 is:
 T1 = T2

ctx_uniq < apply member_nominal_absurd to H4.
Subgoal 2:

Variables: E T1 T2 L1 B
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H1 : ctx (B :: L1)
H3 : member (of E T2) (B :: L1)
H4 : member (of E T1) L1 *
============================
 T1 = T2

ctx_uniq < case H3.
Subgoal 2.1:

Variables: E T1 T2 L1
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H1 : ctx (of E T2 :: L1)
H4 : member (of E T1) L1 *
============================
 T1 = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < case H1.
Subgoal 2.1:

Variables: T1 T2 L2
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H4 : member (of n1 T1) L2 *
H5 : ctx L2
============================
 T1 = T2

Subgoal 2.2 is:
 T1 = T2

ctx_uniq < apply member_nominal_absurd to H4.
Subgoal 2.2:

Variables: E T1 T2 L1 B
IH : forall L E T1 T2, ctx L -> member (of E T1) L * -> member (of E T2) L ->
       T1 =
     T2
H1 : ctx (B :: L1)
H4 : member (of E T1) L1 *
H5 : member (of E T2) L1
============================
 T1 = T2

ctx_uniq < case H1.
Subgoal 2.2:

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

ctx_uniq < apply IH to H6 H4 H5.
Subgoal 2.2:

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

ctx_uniq < search.
Proof completed.
Abella < Theorem ctx_mem : 
forall L E, ctx L -> member E L -> (exists N X, E = of X N /\ name X).


============================
 forall L E, ctx L -> member E L -> (exists N X, E = of X N /\ name X)

ctx_mem < induction on 2.

IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X)
============================
 forall L E, ctx L -> member E L @ -> (exists N X, E = of X N /\ name X)

ctx_mem < intros.

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

ctx_mem < case H2.
Subgoal 1:

Variables: E L1
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X)
H1 : ctx (E :: L1)
============================
 exists N X, E = of X N /\ name X

Subgoal 2 is:
 exists N X, E = of X N /\ name X

ctx_mem < case H1.
Subgoal 1:

Variables: L2 T
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X)
H3 : ctx L2
============================
 exists N X, of n1 T = of X N /\ name X

Subgoal 2 is:
 exists N X, E = of X N /\ name X

ctx_mem < search.
Subgoal 2:

Variables: E L1 B
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X)
H1 : ctx (B :: L1)
H3 : member E L1 *
============================
 exists N X, E = of X N /\ name X

ctx_mem < case H1.
Subgoal 2:

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

ctx_mem < apply IH to H4 H3.
Subgoal 2:

Variables: L2 T N X
IH : forall L E, ctx L -> member E L * -> (exists N X, E = of X N /\ name X)
H3 : member (of (X n1) N) L2 *
H4 : ctx L2
H5 : name (X n1)
============================
 exists N1 X1, of (X n1) N = of X1 N1 /\ name X1

ctx_mem < search.
Proof completed.
Abella < Theorem type_uniq_ext : 
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_ext < 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_ext < 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_ext < 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_ext < 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_ext < 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_ext < 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_ext < apply ctx_mem to H1 H6.
Subgoal 1.2:

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

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq_ext < case H7.
Subgoal 1.2:

Variables: L T2 U R T N
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 |- of (R n2 n1) U}*
H5 : {L n2, [of n2 N] |- of (abs T (R n2)) T2}
H6 : member (of n2 N) (L n2)
============================
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq_ext < 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_ext < 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_ext < 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_ext < 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_ext < apply ctx_mem to H1 H7.
Subgoal 2.2:

Variables: L T1 T2 U N M N1 X
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 N1] |- of (app M N) T2}
H7 : member (of X N1) L
H8 : name X
============================
 T1 = T2

Subgoal 3 is:
 T1 = T2

type_uniq_ext < case H8.
Subgoal 2.2:

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

Subgoal 3 is:
 T1 = T2

type_uniq_ext < 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_ext < apply ctx_mem to H1 H5.
Subgoal 3:

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

type_uniq_ext < case H4.
Subgoal 3:

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_ext < case H6.
Subgoal 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)
H3 : {L n1 |- of n1 T2}
H5 : member (of n1 T1) (L n1)
============================
 T1 = T2

type_uniq_ext < case H3.
Subgoal 3:

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) (L n1)
H7 : {L n1, [F1 n1] |- of n1 T2}
H8 : member (F1 n1) (L n1)
============================
 T1 = T2

type_uniq_ext < apply ctx_mem to H1 H8.
Subgoal 3:

Variables: L T1 T2 N1 X1
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) (L n1)
H7 : {L n1, [of (X1 n1) N1] |- of n1 T2}
H8 : member (of (X1 n1) N1) (L n1)
H9 : name (X1 n1)
============================
 T1 = T2

type_uniq_ext < case H7.
Subgoal 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) (L n1)
H8 : member (of n1 T2) (L n1)
H9 : name n1
============================
 T1 = T2

type_uniq_ext < apply ctx_uniq to H1 H5 H8.
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 n1)
H5 : member (of n1 T2) (L n1)
H8 : member (of n1 T2) (L n1)
H9 : name n1
============================
 T2 = T2

type_uniq_ext < search.
Proof completed.
Abella < Theorem type_uniq : 
forall E T1 T2, {of E T1} -> {of E T2} -> T1 = T2.


============================
 forall E T1 T2, {of E T1} -> {of E T2} -> T1 = T2

type_uniq < intros.

Variables: E T1 T2
H1 : {of E T1}
H2 : {of E T2}
============================
 T1 = T2

type_uniq < apply type_uniq_ext to _ H1 H2.

Variables: E T2
H1 : {of E T2}
H2 : {of E T2}
============================
 T2 = T2

type_uniq < search.
Proof completed.
Abella <