Welcome to Abella 2.0.3-dev
```Abella < Specification "stlc".
```
```Abella < Theorem ty_indep_tm_simp :
forall T, nabla x, {tm x |- ty (T x)} -> (exists T', T = y\T' /\ {ty T'}).
```
```
============================
forall T, nabla x, {tm x |- ty (T x)} -> (exists T', T = y\T' /\ {ty T'})

ty_indep_tm_simp < induction on 1.
```
```
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
============================
forall T, nabla x, {tm x |- ty (T x)}@ -> (exists T', T = y\T' /\ {ty T'})

ty_indep_tm_simp < intros.
```
```
Variables: T
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
H1 : {tm n1 |- ty (T n1)}@
============================
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H1.
```
```Subgoal 1:

IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
============================
exists T', z1\b = y\T' /\ {ty T'}

Subgoal 2 is:
exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {ty T'}

Subgoal 3 is:
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < search.
```
```Subgoal 2:

Variables: T2 T1
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
H2 : {tm n1 |- ty (T1 n1)}*
H3 : {tm n1 |- ty (T2 n1)}*
============================
exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {ty T'}

Subgoal 3 is:
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < apply IH to H2.
```
```Subgoal 2:

Variables: T2 T'
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
H2 : {tm n1 |- ty T'}*
H3 : {tm n1 |- ty (T2 n1)}*
H4 : {ty T'}
============================
exists T'1, z1\arr T' (T2 z1) = y\T'1 /\ {ty T'1}

Subgoal 3 is:
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < apply IH to H3.
```
```Subgoal 2:

Variables: T' T'1
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
H2 : {tm n1 |- ty T'}*
H3 : {tm n1 |- ty T'1}*
H4 : {ty T'}
H5 : {ty T'1}
============================
exists T'2, z1\arr T' T'1 = y\T'2 /\ {ty T'2}

Subgoal 3 is:
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < search.
```
```Subgoal 3:

Variables: T F
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
H2 : {tm n1, [F n1] |- ty (T n1)}*
H3 : member (F n1) (tm n1 :: nil)
============================
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H3.
```
```Subgoal 3.1:

Variables: T
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
H2 : {tm n1, [tm n1] |- ty (T n1)}*
============================
exists T', T = y\T' /\ {ty T'}

Subgoal 3.2 is:
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H2.
```
```Subgoal 3.2:

Variables: T F
IH : forall T, nabla x, {tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {ty T'})
H2 : {tm n1, [F n1] |- ty (T n1)}*
H4 : member (F n1) nil
============================
exists T', T = y\T' /\ {ty T'}

ty_indep_tm_simp < case H4.
Proof completed.
```
```Abella < Define name : tm ->
prop by
nabla x, name x.
```
```Abella < Define ctx : olist ->
prop by
ctx nil;
nabla x, ctx (tm x :: L) := ctx L.
```
```Abella < Theorem ctx_mem :
forall L E, ctx L -> member E L -> (exists X, E = tm X /\ name X).
```
```
============================
forall L E, ctx L -> member E L -> (exists X, E = tm X /\ name X)

ctx_mem < induction on 2.
```
```
IH : forall L E, ctx L -> member E L * -> (exists X, E = tm X /\ name X)
============================
forall L E, ctx L -> member E L @ -> (exists X, E = tm X /\ name X)

ctx_mem < intros.
```
```
Variables: L E
IH : forall L E, ctx L -> member E L * -> (exists X, E = tm X /\ name X)
H1 : ctx L
H2 : member E L @
============================
exists X, E = tm X /\ name X

ctx_mem < case H2.
```
```Subgoal 1:

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

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

ctx_mem < case H1.
```
```Subgoal 1:

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

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

ctx_mem < search.
```
```Subgoal 2:

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

ctx_mem < case H1.
```
```Subgoal 2:

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

ctx_mem < apply IH to H4 H3.
```
```Subgoal 2:

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

ctx_mem < search.
Proof completed.
```
```Abella < Theorem ty_indep_tm :
forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)} ->
(exists T', T = y\T' /\ {L |- ty T'}).
```
```
============================
forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)} ->
(exists T', T = y\T' /\ {L |- ty T'})

ty_indep_tm < induction on 2.
```
```
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
============================
forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}@ ->
(exists T', T = y\T' /\ {L |- ty T'})

ty_indep_tm < intros.
```
```
Variables: L T
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H2 : {L, tm n1 |- ty (T n1)}@
============================
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < case H2.
```
```Subgoal 1:

Variables: L
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
============================
exists T', z1\b = y\T' /\ {L |- ty T'}

Subgoal 2 is:
exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {L |- ty T'}

Subgoal 3 is:
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < search.
```
```Subgoal 2:

Variables: L T2 T1
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1 |- ty (T1 n1)}*
H4 : {L, tm n1 |- ty (T2 n1)}*
============================
exists T', z1\arr (T1 z1) (T2 z1) = y\T' /\ {L |- ty T'}

Subgoal 3 is:
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < apply IH to _ H3.
```
```Subgoal 2:

Variables: L T2 T'
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1 |- ty T'}*
H4 : {L, tm n1 |- ty (T2 n1)}*
H5 : {L |- ty T'}
============================
exists T'1, z1\arr T' (T2 z1) = y\T'1 /\ {L |- ty T'1}

Subgoal 3 is:
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < apply IH to _ H4.
```
```Subgoal 2:

Variables: L T' T'1
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1 |- ty T'}*
H4 : {L, tm n1 |- ty T'1}*
H5 : {L |- ty T'}
H6 : {L |- ty T'1}
============================
exists T'2, z1\arr T' T'1 = y\T'2 /\ {L |- ty T'2}

Subgoal 3 is:
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < search.
```
```Subgoal 3:

Variables: L T F
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1, [F n1] |- ty (T n1)}*
H4 : member (F n1) (tm n1 :: L)
============================
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < case H4.
```
```Subgoal 3.1:

Variables: L T
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1, [tm n1] |- ty (T n1)}*
============================
exists T', T = y\T' /\ {L |- ty T'}

Subgoal 3.2 is:
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < case H3.
```
```Subgoal 3.2:

Variables: L T F
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1, [F n1] |- ty (T n1)}*
H5 : member (F n1) L
============================
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < apply ctx_mem to H1 H5.
```
```Subgoal 3.2:

Variables: L T X
IH : forall L T, nabla x, ctx L -> {L, tm x |- ty (T x)}* ->
(exists T', T = y\T' /\ {L |- ty T'})
H1 : ctx L
H3 : {L, tm n1, [tm (X n1)] |- ty (T n1)}*
H5 : member (tm (X n1)) L
H6 : name (X n1)
============================
exists T', T = y\T' /\ {L |- ty T'}

ty_indep_tm < case H3.
Proof completed.
```
```Abella < Goodbye.
```