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

Abella < Theorem member_prune : 
forall E L, nabla x, member (E x) L -> (exists F, E = y\F).


============================
 forall E L, nabla x, member (E x) L -> (exists F, E = y\F)

member_prune < induction on 1.

IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
 forall E L, nabla x, member (E x) L @ -> (exists F, E = y\F)

member_prune < intros.

Variables: E L
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H1 : member (E n1) L @
============================
 exists F, E = y\F

member_prune < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
 exists F, z1\L2 = y\F

Subgoal 2 is:
 exists F, E = y\F

member_prune < search.
Subgoal 2:

Variables: E L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member (E n1) L3 *
============================
 exists F, E = y\F

member_prune < apply IH to H2.
Subgoal 2:

Variables: L3 L2 F
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member F L3 *
============================
 exists F1, z1\F = y\F1

member_prune < search.
Proof completed.
Abella < Define ctx : olist -> prop by 
ctx nil;
ctx (of X T :: L) := (forall M N, X = app M N -> false) /\ (forall T R, X = abs T R -> false) /\
  (forall T', member (of X T') L -> false) /\ ctx L.

Abella < Theorem ctx_member : 
forall E L, ctx L -> member E L ->
  (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
       (forall T R, X = abs T R -> false)).


============================
 forall E L, ctx L -> member E L ->
   (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
        (forall T R, X = abs T R -> false))

ctx_member < induction on 1.

IH : forall E L, ctx L * -> member E L ->
       (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
            (forall T R, X = abs T R -> false))
============================
 forall E L, ctx L @ -> member E L ->
   (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
        (forall T R, X = abs T R -> false))

ctx_member < intros.

Variables: E L
IH : forall E L, ctx L * -> member E L ->
       (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
            (forall T R, X = abs T R -> false))
H1 : ctx L @
H2 : member E L
============================
 exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
   (forall T R, X = abs T R -> false)

ctx_member < case H1.
Subgoal 1:

Variables: E
IH : forall E L, ctx L * -> member E L ->
       (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
            (forall T1 R, X = abs T1 R -> false))
H2 : member E nil
============================
 exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
   (forall T1 R, X = abs T1 R -> false)

Subgoal 2 is:
 exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
   (forall T1 R, X = abs T1 R -> false)

ctx_member < case H2.
Subgoal 2:

Variables: E L1 T X
IH : forall E L, ctx L * -> member E L ->
       (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
            (forall T1 R, X = abs T1 R -> false))
H2 : member E (of X T :: L1)
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
============================
 exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
   (forall T1 R, X = abs T1 R -> false)

ctx_member < case H2.
Subgoal 2.1:

Variables: L1 T X
IH : forall E L, ctx L * -> member E L ->
       (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
            (forall T1 R, X = abs T1 R -> false))
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
============================
 exists X1 T1, of X T = of X1 T1 /\ (forall M N, X1 = app M N -> false) /\
   (forall T2 R, X1 = abs T2 R -> false)

Subgoal 2.2 is:
 exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
   (forall T1 R, X = abs T1 R -> false)

ctx_member < search.
Subgoal 2.2:

Variables: E L1 T X
IH : forall E L, ctx L * -> member E L ->
       (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
            (forall T1 R, X = abs T1 R -> false))
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
H7 : member E L1
============================
 exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
   (forall T1 R, X = abs T1 R -> false)

ctx_member < apply IH to H6 H7.
Subgoal 2.2:

Variables: L1 T X X1 T1
IH : forall E L, ctx L * -> member E L ->
       (exists X T, E = of X T /\ (forall M N, X = app M N -> false) /\
            (forall T1 R, X = abs T1 R -> false))
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
H7 : member (of X1 T1) L1
H8 : forall M N, X1 = app M N -> false
H9 : forall T2 R, X1 = abs T2 R -> false
============================
 exists X T, of X1 T1 = of X T /\ (forall M N, X = app M N -> false) /\
   (forall T2 R, X = abs T2 R -> false)

ctx_member < search.
Proof completed.
Abella < Theorem ctx_app_absurd : 
forall L M N T, ctx L -> member (of (app M N) T) L -> false.


============================
 forall L M N T, ctx L -> member (of (app M N) T) L -> false

ctx_app_absurd < induction on 1.

IH : forall L M N T, ctx L * -> member (of (app M N) T) L -> false
============================
 forall L M N T, ctx L @ -> member (of (app M N) T) L -> false

ctx_app_absurd < intros.

Variables: L M N T
IH : forall L M N T, ctx L * -> member (of (app M N) T) L -> false
H1 : ctx L @
H2 : member (of (app M N) T) L
============================
 false

ctx_app_absurd < case H1.
Subgoal 1:

Variables: M N T
IH : forall L M N T, ctx L * -> member (of (app M N) T) L -> false
H2 : member (of (app M N) T) nil
============================
 false

Subgoal 2 is:
 false

ctx_app_absurd < case H2.
Subgoal 2:

Variables: M N T L1 T1 X
IH : forall L M N T, ctx L * -> member (of (app M N) T) L -> false
H2 : member (of (app M N) T) (of X T1 :: L1)
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
============================
 false

ctx_app_absurd < case H2.
Subgoal 2.1:

Variables: M N L1 T1
IH : forall L M N T, ctx L * -> member (of (app M N) T) L -> false
H3 : forall M1 N1, app M N = app M1 N1 -> false
H4 : forall T R, app M N = abs T R -> false
H5 : forall T', member (of (app M N) T') L1 -> false
H6 : ctx L1 *
============================
 false

Subgoal 2.2 is:
 false

ctx_app_absurd < apply H3 to _.
Subgoal 2.2:

Variables: M N T L1 T1 X
IH : forall L M N T, ctx L * -> member (of (app M N) T) L -> false
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
H7 : member (of (app M N) T) L1
============================
 false

ctx_app_absurd < apply IH to H6 H7.
Proof completed.
Abella < Theorem ctx_abs_absurd : 
forall L R T S, ctx L -> member (of (abs S R) T) L -> false.


============================
 forall L R T S, ctx L -> member (of (abs S R) T) L -> false

ctx_abs_absurd < induction on 1.

IH : forall L R T S, ctx L * -> member (of (abs S R) T) L -> false
============================
 forall L R T S, ctx L @ -> member (of (abs S R) T) L -> false

ctx_abs_absurd < intros.

Variables: L R T S
IH : forall L R T S, ctx L * -> member (of (abs S R) T) L -> false
H1 : ctx L @
H2 : member (of (abs S R) T) L
============================
 false

ctx_abs_absurd < case H1.
Subgoal 1:

Variables: R T S
IH : forall L R T S, ctx L * -> member (of (abs S R) T) L -> false
H2 : member (of (abs S R) T) nil
============================
 false

Subgoal 2 is:
 false

ctx_abs_absurd < case H2.
Subgoal 2:

Variables: R T S L1 T1 X
IH : forall L R T S, ctx L * -> member (of (abs S R) T) L -> false
H2 : member (of (abs S R) T) (of X T1 :: L1)
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
============================
 false

ctx_abs_absurd < case H2.
Subgoal 2.1:

Variables: R S L1 T1
IH : forall L R T S, ctx L * -> member (of (abs S R) T) L -> false
H3 : forall M N, abs S R = app M N -> false
H4 : forall T R1, abs S R = abs T R1 -> false
H5 : forall T', member (of (abs S R) T') L1 -> false
H6 : ctx L1 *
============================
 false

Subgoal 2.2 is:
 false

ctx_abs_absurd < apply H4 to _.
Subgoal 2.2:

Variables: R T S L1 T1 X
IH : forall L R T S, ctx L * -> member (of (abs S R) T) L -> false
H3 : forall M N, X = app M N -> false
H4 : forall T R, X = abs T R -> false
H5 : forall T', member (of X T') L1 -> false
H6 : ctx L1 *
H7 : member (of (abs S R) T) L1
============================
 false

ctx_abs_absurd < apply IH to H6 H7.
Proof completed.
Abella < Theorem 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

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

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

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

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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
============================
 T1 = T2

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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
============================
 T = T2

Subgoal 2.2 is:
 T1 = T2

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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
============================
 T = T

Subgoal 2.1.2 is:
 T = T2

Subgoal 2.2 is:
 T1 = T2

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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
H8 : member (of X T2) L1
============================
 T = T2

Subgoal 2.2 is:
 T1 = T2

uniq < apply H6 to H8.
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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
H8 : member (of E T1) L1
============================
 T1 = T2

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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
H8 : member (of X T1) L1
============================
 T1 = T

Subgoal 2.2.2 is:
 T1 = T2

uniq < apply H6 to H8.
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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
H8 : member (of E T1) L1
H9 : member (of E T2) L1
============================
 T1 = T2

uniq < apply IH to H7 H8 H9.
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 : forall M N, X = app M N -> false
H5 : forall T R, X = abs T R -> false
H6 : forall T', member (of X T') L1 -> false
H7 : ctx L1 *
H8 : member (of E T2) L1
H9 : member (of E T2) L1
============================
 T2 = T2

uniq < search.
Proof completed.
Abella < Theorem ctx_extend : 
forall T L, nabla x, ctx L -> ctx (of x T :: L).


============================
 forall T L, nabla x, ctx L -> ctx (of x T :: L)

ctx_extend < intros.

Variables: T L
H1 : ctx L
============================
 ctx (of n1 T :: L)

ctx_extend < unfold.
Subgoal 1:

Variables: T L
H1 : ctx L
============================
 forall M N, n1 = app M N -> false

Subgoal 2 is:
 forall T R, n1 = abs T R -> false

Subgoal 3 is:
 forall T', member (of n1 T') L -> false

Subgoal 4 is:
 ctx L

ctx_extend < intros.
Subgoal 1:

Variables: T L M N
H1 : ctx L
H2 : n1 = app (M n1) (N n1)
============================
 false

Subgoal 2 is:
 forall T R, n1 = abs T R -> false

Subgoal 3 is:
 forall T', member (of n1 T') L -> false

Subgoal 4 is:
 ctx L

ctx_extend < case H2.
Subgoal 2:

Variables: T L
H1 : ctx L
============================
 forall T R, n1 = abs T R -> false

Subgoal 3 is:
 forall T', member (of n1 T') L -> false

Subgoal 4 is:
 ctx L

ctx_extend < intros.
Subgoal 2:

Variables: T L T1 R
H1 : ctx L
H2 : n1 = abs (T1 n1) (R n1)
============================
 false

Subgoal 3 is:
 forall T', member (of n1 T') L -> false

Subgoal 4 is:
 ctx L

ctx_extend < case H2.
Subgoal 3:

Variables: T L
H1 : ctx L
============================
 forall T', member (of n1 T') L -> false

Subgoal 4 is:
 ctx L

ctx_extend < intros.
Subgoal 3:

Variables: T L T'
H1 : ctx L
H2 : member (of n1 (T' n1)) L
============================
 false

Subgoal 4 is:
 ctx L

ctx_extend < apply member_prune to H2.
Subgoal 4:

Variables: T L
H1 : ctx L
============================
 ctx L

ctx_extend < search.
Proof completed.
Abella < Theorem det_of : 
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

det_of < 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

det_of < 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

det_of < 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

det_of < 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

det_of < apply IH to _ H4 H5.
Subgoal 1.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}
============================
 ctx (of n1 T :: L)

Subgoal 1.1 is:
 arrow T U1 = arrow T U1

Subgoal 1.2 is:
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

det_of < backchain ctx_extend.
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

det_of < 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

det_of < apply ctx_member 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 : forall M N, X = app M N -> false
H8 : forall T1 R, X = abs T1 R -> false
============================
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

det_of < case H5.
Subgoal 1.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 : forall M N, abs T R = app M N -> false
H8 : forall T1 R1, abs T R = abs T1 R1 -> false
============================
 arrow T U = T2

Subgoal 2 is:
 T1 = T2

Subgoal 3 is:
 T1 = T2

det_of < apply H8 to _ with T1 = T, R1 = R.
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

det_of < 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

det_of < apply IH to _ 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

det_of < 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

det_of < apply ctx_member 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 : forall M N, X = app M N -> false
H9 : forall T1 R, X = abs T1 R -> false
============================
 T1 = T2

Subgoal 3 is:
 T1 = T2

det_of < case H6.
Subgoal 2.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 (arrow U T1)}*
H5 : {L |- of N U}*
H7 : member (of (app M N) T2) L
H8 : forall M1 N1, app M N = app M1 N1 -> false
H9 : forall T1 R, app M N = abs T1 R -> false
============================
 T1 = T2

Subgoal 3 is:
 T1 = T2

det_of < apply H8 to _ with M1 = M, N1 = N.
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

det_of < apply ctx_member 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 : forall M N, X = app M N -> false
H7 : forall T1 R, X = abs T1 R -> false
============================
 T1 = T2

det_of < 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 : forall M N, E = app M N -> false
H7 : forall T1 R, E = abs T1 R -> false
============================
 T1 = T2

det_of < case H3.
Subgoal 3.1:

Variables: L T1 U R T3
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx L
H5 : member (of (abs T3 R) T1) L
H6 : forall M N, abs T3 R = app M N -> false
H7 : forall T1 R1, abs T3 R = abs T1 R1 -> false
H8 : {L, of n1 T3 |- of (R n1) U}
============================
 T1 = arrow T3 U

Subgoal 3.2 is:
 T1 = T2

Subgoal 3.3 is:
 T1 = T2

det_of < apply H7 to _ with T1 = T3, R1 = R.
Subgoal 3.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
H5 : member (of (app M N) T1) L
H6 : forall M1 N1, app M N = app M1 N1 -> false
H7 : forall T1 R, app M N = abs T1 R -> false
H8 : {L |- of M (arrow U T2)}
H9 : {L |- of N U}
============================
 T1 = T2

Subgoal 3.3 is:
 T1 = T2

det_of < apply H6 to _ with M1 = M, N1 = N.
Subgoal 3.3:

Variables: L E T1 T2 F1
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx L
H5 : member (of E T1) L
H6 : forall M N, E = app M N -> false
H7 : forall T1 R, E = abs T1 R -> false
H8 : {L, [F1] |- of E T2}
H9 : member F1 L
============================
 T1 = T2

det_of < apply ctx_member to H1 H9.
Subgoal 3.3:

Variables: L E T1 T2 X1 T3
IH : forall L E T1 T2, ctx L -> {L |- of E T1}* -> {L |- of E T2} -> T1 = T2
H1 : ctx L
H5 : member (of E T1) L
H6 : forall M N, E = app M N -> false
H7 : forall T1 R, E = abs T1 R -> false
H8 : {L, [of X1 T3] |- of E T2}
H9 : member (of X1 T3) L
H10 : forall M N, X1 = app M N -> false
H11 : forall T1 R, X1 = abs T1 R -> false
============================
 T1 = T2

det_of < case H8.
Subgoal 3.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
H5 : member (of E T1) L
H6 : forall M N, E = app M N -> false
H7 : forall T1 R, E = abs T1 R -> false
H9 : member (of E T2) L
H10 : forall M N, E = app M N -> false
H11 : forall T1 R, E = abs T1 R -> false
============================
 T1 = T2

det_of < apply uniq to H1 H5 H9.
Subgoal 3.3:

Variables: L E 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 E T2) L
H6 : forall M N, E = app M N -> false
H7 : forall T1 R, E = abs T1 R -> false
H9 : member (of E T2) L
H10 : forall M N, E = app M N -> false
H11 : forall T1 R, E = abs T1 R -> false
============================
 T2 = T2

det_of < search.
Proof completed.
Abella <