Welcome to Abella 2.0.5-dev.
```Abella < Kind tm type.

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

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

```
```Abella < Type pair tm -> tm -> o.

```
```Abella < Define subst : olist -> tm -> tm -> prop by
subst nil T T;
nabla x, subst (pair x K :: L) (T x) S := subst L (T K) S.

```
```Abella < Theorem subst_app :
forall L T R S, subst L (app T R) S ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V).

```
```
============================
forall L T R S, subst L (app T R) S ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V)

subst_app < induction on 1.
```
```
IH : forall L T R S, subst L (app T R) S * ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V)
============================
forall L T R S, subst L (app T R) S @ ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V)

subst_app < intros.
```
```
Variables: L T R S
IH : forall L T R S, subst L (app T R) S * ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V)
H1 : subst L (app T R) S @
============================
exists U V, S = app U V /\ subst L T U /\ subst L R V

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

Variables: T R
IH : forall L T R S, subst L (app T R) S * ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V)
============================
exists U V, app T R = app U V /\ subst nil T U /\ subst nil R V

Subgoal 2 is:
exists U V, S1 = app U V /\ subst (pair n1 K :: L1) (T n1) U /\
subst (pair n1 K :: L1) (R n1) V

subst_app < search.
```
```Subgoal 2:

Variables: T R S1 L1 K
IH : forall L T R S, subst L (app T R) S * ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V)
H2 : subst L1 (app (T K) (R K)) S1 *
============================
exists U V, S1 = app U V /\ subst (pair n1 K :: L1) (T n1) U /\
subst (pair n1 K :: L1) (R n1) V

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

Variables: T R L1 K U V
IH : forall L T R S, subst L (app T R) S * ->
(exists U V, S = app U V /\ subst L T U /\ subst L R V)
H2 : subst L1 (app (T K) (R K)) (app U V) *
H3 : subst L1 (T K) U
H4 : subst L1 (R K) V
============================
exists U1 V1, app U V = app U1 V1 /\ subst (pair n1 K :: L1) (T n1) U1 /\
subst (pair n1 K :: L1) (R n1) V1

subst_app < search.
Proof completed.
```
```Abella < Theorem subst_abs :
forall L T R, subst L (abs T) R ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z))).

```
```
============================
forall L T R, subst L (abs T) R ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z)))

subst_abs < induction on 1.
```
```
IH : forall L T R, subst L (abs T) R * ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z)))
============================
forall L T R, subst L (abs T) R @ ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z)))

subst_abs < intros.
```
```
Variables: L T R
IH : forall L T R, subst L (abs T) R * ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z)))
H1 : subst L (abs T) R @
============================
exists S, R = abs S /\ (nabla z, subst L (T z) (S z))

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

Variables: T
IH : forall L T R, subst L (abs T) R * ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z)))
============================
exists S, abs T = abs S /\ (nabla z, subst nil (T z) (S z))

Subgoal 2 is:
exists S1, S = abs S1 /\ (nabla z, subst (pair n1 K :: L1) (T n1 z) (S1 z))

subst_abs < search.
```
```Subgoal 2:

Variables: T S L1 K
IH : forall L T R, subst L (abs T) R * ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z)))
H2 : subst L1 (abs (T K)) S *
============================
exists S1, S = abs S1 /\ (nabla z, subst (pair n1 K :: L1) (T n1 z) (S1 z))

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

Variables: T L1 K S1
IH : forall L T R, subst L (abs T) R * ->
(exists S, R = abs S /\ (nabla z, subst L (T z) (S z)))
H2 : subst L1 (abs (T K)) (abs S1) *
H3 : subst L1 (T K n1) (S1 n1)
============================
exists S2, abs S1 = abs S2 /\
(nabla z, subst (pair n1 K :: L1) (T n1 z) (S2 z))

subst_abs < search.
Proof completed.
```
```Abella <
```