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

Abella < Define ctx : olist -> olist -> prop by 
ctx nil nil;
ctx (term X :: L) (copy X X :: K) := ctx L K.

Abella < Theorem ctx_member1 : 
forall L K E, ctx L K -> member E L ->
  (exists T, E = term T /\ member (copy T T) K).


============================
 forall L K E, ctx L K -> member E L ->
   (exists T, E = term T /\ member (copy T T) K)

ctx_member1 < induction on 1.

IH : forall L K E, ctx L K * -> member E L ->
       (exists T, E = term T /\ member (copy T T) K)
============================
 forall L K E, ctx L K @ -> member E L ->
   (exists T, E = term T /\ member (copy T T) K)

ctx_member1 < intros.

Variables: L K E
IH : forall L K E, ctx L K * -> member E L ->
       (exists T, E = term T /\ member (copy T T) K)
H1 : ctx L K @
H2 : member E L
============================
 exists T, E = term T /\ member (copy T T) K

ctx_member1 < case H1.
Subgoal 1:

Variables: E
IH : forall L K E, ctx L K * -> member E L ->
       (exists T, E = term T /\ member (copy T T) K)
H2 : member E nil
============================
 exists T, E = term T /\ member (copy T T) nil

Subgoal 2 is:
 exists T, E = term T /\ member (copy T T) (copy X X :: K1)

ctx_member1 < case H2.
Subgoal 2:

Variables: E K1 X L1
IH : forall L K E, ctx L K * -> member E L ->
       (exists T, E = term T /\ member (copy T T) K)
H2 : member E (term X :: L1)
H3 : ctx L1 K1 *
============================
 exists T, E = term T /\ member (copy T T) (copy X X :: K1)

ctx_member1 < case H2.
Subgoal 2.1:

Variables: K1 X L1
IH : forall L K E, ctx L K * -> member E L ->
       (exists T, E = term T /\ member (copy T T) K)
H3 : ctx L1 K1 *
============================
 exists T, term X = term T /\ member (copy T T) (copy X X :: K1)

Subgoal 2.2 is:
 exists T, E = term T /\ member (copy T T) (copy X X :: K1)

ctx_member1 < search.
Subgoal 2.2:

Variables: E K1 X L1
IH : forall L K E, ctx L K * -> member E L ->
       (exists T, E = term T /\ member (copy T T) K)
H3 : ctx L1 K1 *
H4 : member E L1
============================
 exists T, E = term T /\ member (copy T T) (copy X X :: K1)

ctx_member1 < apply IH to H3 H4.
Subgoal 2.2:

Variables: K1 X L1 T
IH : forall L K E, ctx L K * -> member E L ->
       (exists T, E = term T /\ member (copy T T) K)
H3 : ctx L1 K1 *
H4 : member (term T) L1
H5 : member (copy T T) K1
============================
 exists T1, term T = term T1 /\ member (copy T1 T1) (copy X X :: K1)

ctx_member1 < search.
Proof completed.
Abella < Theorem ctx_member2 : 
forall L K E, ctx L K -> member E K -> (exists T, E = copy T T).


============================
 forall L K E, ctx L K -> member E K -> (exists T, E = copy T T)

ctx_member2 < induction on 1.

IH : forall L K E, ctx L K * -> member E K -> (exists T, E = copy T T)
============================
 forall L K E, ctx L K @ -> member E K -> (exists T, E = copy T T)

ctx_member2 < intros.

Variables: L K E
IH : forall L K E, ctx L K * -> member E K -> (exists T, E = copy T T)
H1 : ctx L K @
H2 : member E K
============================
 exists T, E = copy T T

ctx_member2 < case H1.
Subgoal 1:

Variables: E
IH : forall L K E, ctx L K * -> member E K -> (exists T, E = copy T T)
H2 : member E nil
============================
 exists T, E = copy T T

Subgoal 2 is:
 exists T, E = copy T T

ctx_member2 < case H2.
Subgoal 2:

Variables: E K1 X L1
IH : forall L K E, ctx L K * -> member E K -> (exists T, E = copy T T)
H2 : member E (copy X X :: K1)
H3 : ctx L1 K1 *
============================
 exists T, E = copy T T

ctx_member2 < case H2.
Subgoal 2.1:

Variables: K1 X L1
IH : forall L K E, ctx L K * -> member E K -> (exists T, E = copy T T)
H3 : ctx L1 K1 *
============================
 exists T, copy X X = copy T T

Subgoal 2.2 is:
 exists T, E = copy T T

ctx_member2 < search.
Subgoal 2.2:

Variables: E K1 X L1
IH : forall L K E, ctx L K * -> member E K -> (exists T, E = copy T T)
H3 : ctx L1 K1 *
H4 : member E K1
============================
 exists T, E = copy T T

ctx_member2 < apply IH to H3 H4.
Subgoal 2.2:

Variables: K1 X L1 T
IH : forall L K E, ctx L K * -> member E K -> (exists T, E = copy T T)
H3 : ctx L1 K1 *
H4 : member (copy T T) K1
============================
 exists T1, copy T T = copy T1 T1

ctx_member2 < search.
Proof completed.
Abella < Theorem copy_id : 
forall L K T, ctx L K -> {L |- term T} -> {K |- copy T T}.


============================
 forall L K T, ctx L K -> {L |- term T} -> {K |- copy T T}

copy_id < induction on 2.

IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
============================
 forall L K T, ctx L K -> {L |- term T}@ -> {K |- copy T T}

copy_id < intros.

Variables: L K T
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H2 : {L |- term T}@
============================
 {K |- copy T T}

copy_id < case H2.
Subgoal 1:

Variables: L K N M
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H3 : {L |- term M}*
H4 : {L |- term N}*
============================
 {K |- copy (app M N) (app M N)}

Subgoal 2 is:
 {K |- copy (abs R) (abs R)}

Subgoal 3 is:
 {K |- copy T T}

copy_id < apply IH to H1 H3.
Subgoal 1:

Variables: L K N M
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H5 : {K |- copy M M}
============================
 {K |- copy (app M N) (app M N)}

Subgoal 2 is:
 {K |- copy (abs R) (abs R)}

Subgoal 3 is:
 {K |- copy T T}

copy_id < apply IH to H1 H4.
Subgoal 1:

Variables: L K N M
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H3 : {L |- term M}*
H4 : {L |- term N}*
H5 : {K |- copy M M}
H6 : {K |- copy N N}
============================
 {K |- copy (app M N) (app M N)}

Subgoal 2 is:
 {K |- copy (abs R) (abs R)}

Subgoal 3 is:
 {K |- copy T T}

copy_id < search.
Subgoal 2:

Variables: L K R
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H3 : {L, term n1 |- term (R n1)}*
============================
 {K |- copy (abs R) (abs R)}

Subgoal 3 is:
 {K |- copy T T}

copy_id < apply IH to _ H3.
Subgoal 2:

Variables: L K R
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H3 : {L, term n1 |- term (R n1)}*
H4 : {K, copy n1 n1 |- copy (R n1) (R n1)}
============================
 {K |- copy (abs R) (abs R)}

Subgoal 3 is:
 {K |- copy T T}

copy_id < search.
Subgoal 3:

Variables: L K T F
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H3 : {L, [F] |- term T}*
H4 : member F L
============================
 {K |- copy T T}

copy_id < apply ctx_member1 to H1 H4.
Subgoal 3:

Variables: L K T T1
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H3 : {L, [term T1] |- term T}*
H4 : member (term T1) L
H5 : member (copy T1 T1) K
============================
 {K |- copy T T}

copy_id < case H3.
Subgoal 3:

Variables: L K T
IH : forall L K T, ctx L K -> {L |- term T}* -> {K |- copy T T}
H1 : ctx L K
H4 : member (term T) L
H5 : member (copy T T) K
============================
 {K |- copy T T}

copy_id < search.
Proof completed.
Abella < Theorem copy_eq : 
forall L K T S, ctx L K -> {K |- copy T S} -> T = S.


============================
 forall L K T S, ctx L K -> {K |- copy T S} -> T = S

copy_eq < induction on 2.

IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
============================
 forall L K T S, ctx L K -> {K |- copy T S}@ -> T = S

copy_eq < intros.

Variables: L K T S
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H2 : {K |- copy T S}@
============================
 T = S

copy_eq < case H2.
Subgoal 1:

Variables: L K Q M P N
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H3 : {K |- copy N P}*
H4 : {K |- copy M Q}*
============================
 app N M = app P Q

Subgoal 2 is:
 abs R = abs S1

Subgoal 3 is:
 T = S

copy_eq < apply IH to H1 H3.
Subgoal 1:

Variables: L K Q M P
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H3 : {K |- copy P P}*
H4 : {K |- copy M Q}*
============================
 app P M = app P Q

Subgoal 2 is:
 abs R = abs S1

Subgoal 3 is:
 T = S

copy_eq < apply IH to H1 H4.
Subgoal 1:

Variables: L K Q P
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H3 : {K |- copy P P}*
H4 : {K |- copy Q Q}*
============================
 app P Q = app P Q

Subgoal 2 is:
 abs R = abs S1

Subgoal 3 is:
 T = S

copy_eq < search.
Subgoal 2:

Variables: L K S1 R
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H3 : {K, copy n1 n1 |- copy (R n1) (S1 n1)}*
============================
 abs R = abs S1

Subgoal 3 is:
 T = S

copy_eq < apply IH to _ H3.
Subgoal 2:

Variables: L K S1
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H3 : {K, copy n1 n1 |- copy (S1 n1) (S1 n1)}*
============================
 abs (z1\S1 z1) = abs S1

Subgoal 3 is:
 T = S

copy_eq < search.
Subgoal 3:

Variables: L K T S F
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H3 : {K, [F] |- copy T S}*
H4 : member F K
============================
 T = S

copy_eq < apply ctx_member2 to H1 H4.
Subgoal 3:

Variables: L K T S T1
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H3 : {K, [copy T1 T1] |- copy T S}*
H4 : member (copy T1 T1) K
============================
 T = S

copy_eq < case H3.
Subgoal 3:

Variables: L K S
IH : forall L K T S, ctx L K -> {K |- copy T S}* -> T = S
H1 : ctx L K
H4 : member (copy S S) K
============================
 S = S

copy_eq < search.
Proof completed.
Abella < Theorem subst : 
forall R T S, {term T} -> {subst R T S} -> R T = S.


============================
 forall R T S, {term T} -> {subst R T S} -> R T = S

subst < intros.

Variables: R T S
H1 : {term T}
H2 : {subst R T S}
============================
 R T = S

subst < case H2.

Variables: R T S
H1 : {term T}
H3 : {copy n1 T |- copy (R n1) S}
============================
 R T = S

subst < apply copy_id to _ H1.

Variables: R T S
H1 : {term T}
H3 : {copy n1 T |- copy (R n1) S}
H4 : {copy T T}
============================
 R T = S

subst <  inst H3 with n1 = T.

Variables: R T S
H1 : {term T}
H3 : {copy n1 T |- copy (R n1) S}
H4 : {copy T T}
H5 : {copy T T |- copy (R T) S}
============================
 R T = S

subst < cut H5 with H4.

Variables: R T S
H1 : {term T}
H3 : {copy n1 T |- copy (R n1) S}
H4 : {copy T T}
H5 : {copy T T |- copy (R T) S}
H6 : {copy (R T) S}
============================
 R T = S

subst < apply copy_eq to _ H6.

Variables: R T
H1 : {term T}
H3 : {copy n1 T |- copy (R n1) (R T)}
H4 : {copy T T}
H5 : {copy T T |- copy (R T) (R T)}
H6 : {copy (R T) (R T)}
============================
 R T = R T

subst < search.
Proof completed.
Abella <