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 <