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 <