Welcome to Abella 2.0.5-dev.
Abella < Kind tm, ty type.

Abella < Type app tm -> tm -> tm.

Abella < Type abs ty -> (tm -> tm) -> tm.

Abella < Type arr ty -> ty -> ty.

Abella < Type bind tm -> ty -> o.

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 (bind x A :: L) := ctx L.

Abella < Define of : olist -> tm -> ty -> prop by 
nabla x, of (L x) x A := nabla x, member (bind x A) (L x);
of L (app M N) B := exists A, of L M (arr A B) /\ of L N A;
of L (abs A R) (arr A B) := nabla x, of (bind x A :: L) (R x) B.

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


============================
 forall L E T1 T2, ctx L -> member (bind E T1) L -> member (bind E T2) L ->
   T1 =
 T2

ctx_uniq < induction on 1.

IH : forall L E T1 T2, ctx L * -> member (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
============================
 forall L E T1 T2, ctx L @ -> member (bind E T1) L -> member (bind E T2) L ->
   T1 =
 T2

ctx_uniq < intros.

Variables: L E T1 T2
IH : forall L E T1 T2, ctx L * -> member (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H1 : ctx L @
H2 : member (bind E T1) L
H3 : member (bind E T2) L
============================
 T1 = T2

ctx_uniq < case H1.
Subgoal 1:

Variables: E T1 T2
IH : forall L E T1 T2, ctx L * -> member (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H2 : member (bind E T1) nil
H3 : member (bind 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 (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H2 : member (bind (E n1) (T1 n1)) (bind n1 A :: L1)
H3 : member (bind (E n1) (T2 n1)) (bind 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 (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H3 : member (bind n1 (T2 n1)) (bind 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 (bind E T1) L ->
       member (bind 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 (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H4 : ctx L1 *
H5 : member (bind 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 (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H3 : member (bind (E n1) (T2 n1)) (bind n1 A :: L1)
H4 : ctx L1 *
H5 : member (bind (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 (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H4 : ctx L1 *
H5 : member (bind 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 (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H4 : ctx L1 *
H5 : member (bind (E n1) (T1 n1)) L1
H6 : member (bind (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 (bind E T1) L ->
       member (bind E T2) L -> T1 =
     T2
H4 : ctx L1 *
H5 : member (bind (E n1) (T2 n1)) L1
H6 : member (bind (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 -> of L E T1 -> of L E T2 -> T1 = T2.


============================
 forall L E T1 T2, ctx L -> of L E T1 -> of L E T2 -> T1 = T2

type_uniq < induction on 2.

IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
============================
 forall L E T1 T2, ctx L -> of L E T1 @ -> of L E T2 -> T1 = T2

type_uniq < intros.

Variables: L E T1 T2
IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
H1 : ctx L
H2 : of L E T1 @
H3 : of L E T2
============================
 T1 = T2

type_uniq < case H2.
Subgoal 1:

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

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 arr A B = T2

type_uniq < case H3.
Subgoal 1:

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

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 arr A B = T2

type_uniq < apply ctx_uniq to H1 H4 H5.
Subgoal 1:

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

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 arr A B = T2

type_uniq < search.
Subgoal 2:

Variables: L T1 T2 A N M
IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
H1 : ctx L
H3 : of L (app M N) T2
H4 : of L M (arr A T1) *
H5 : of L N A *
============================
 T1 = T2

Subgoal 3 is:
 arr A B = T2

type_uniq < case H3.
Subgoal 2:

Variables: L T1 T2 A N M A1
IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
H1 : ctx L
H4 : of L M (arr A T1) *
H5 : of L N A *
H6 : of L M (arr A1 T2)
H7 : of L N A1
============================
 T1 = T2

Subgoal 3 is:
 arr A B = T2

type_uniq < apply IH to H1 H4 H6.
Subgoal 2:

Variables: L T2 N M A1
IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
H1 : ctx L
H4 : of L M (arr A1 T2) *
H5 : of L N A1 *
H6 : of L M (arr A1 T2)
H7 : of L N A1
============================
 T2 = T2

Subgoal 3 is:
 arr A B = T2

type_uniq < search.
Subgoal 3:

Variables: L T2 B A R
IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
H1 : ctx L
H3 : of L (abs A R) T2
H4 : of (bind n1 A :: L) (R n1) B *
============================
 arr A B = T2

type_uniq < case H3.
Subgoal 3:

Variables: L B A R B1
IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
H1 : ctx L
H4 : of (bind n1 A :: L) (R n1) B *
H5 : of (bind n1 A :: L) (R n1) B1
============================
 arr A B = arr A B1

type_uniq < apply IH to _ H4 H5.
Subgoal 3:

Variables: L A R B1
IH : forall L E T1 T2, ctx L -> of L E T1 * -> of L E T2 -> T1 = T2
H1 : ctx L
H4 : of (bind n1 A :: L) (R n1) B1 *
H5 : of (bind n1 A :: L) (R n1) B1
============================
 arr A B1 = arr A B1

type_uniq < search.
Proof completed.
Abella <