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

Abella < Theorem member_prune : 
forall E L, nabla x, member (E x) L -> (exists F, E = y\F).


============================
 forall E L, nabla x, member (E x) L -> (exists F, E = y\F)

member_prune < induction on 1.

IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
 forall E L, nabla x, member (E x) L @ -> (exists F, E = y\F)

member_prune < intros.

Variables: E L
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H1 : member (E n1) L @
============================
 exists F, E = y\F

member_prune < case H1.
Subgoal 1:

Variables: L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
============================
 exists F, z1\L2 = y\F

Subgoal 2 is:
 exists F, E = y\F

member_prune < search.
Subgoal 2:

Variables: E L3 L2
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member (E n1) L3 *
============================
 exists F, E = y\F

member_prune < apply IH to H2.
Subgoal 2:

Variables: L3 L2 F
IH : forall E L, nabla x, member (E x) L * -> (exists F, E = y\F)
H2 : member F L3 *
============================
 exists F1, z1\F = y\F1

member_prune < search.
Proof completed.
Abella < Define ctx : olist -> olist -> prop by 
ctx nil nil;
nabla x, ctx (tm x :: C) (sred x x :: D) := ctx C D.

Abella < Theorem ctx_member1 : 
forall C D H, ctx C D -> member H C ->
  (exists X, H = tm X /\ member (sred X X) D).


============================
 forall C D H, ctx C D -> member H C ->
   (exists X, H = tm X /\ member (sred X X) D)

ctx_member1 < induction on 2.

IH : forall C D H, ctx C D -> member H C * ->
       (exists X, H = tm X /\ member (sred X X) D)
============================
 forall C D H, ctx C D -> member H C @ ->
   (exists X, H = tm X /\ member (sred X X) D)

ctx_member1 < intros.

Variables: C D H
IH : forall C D H, ctx C D -> member H C * ->
       (exists X, H = tm X /\ member (sred X X) D)
H1 : ctx C D
H2 : member H C @
============================
 exists X, H = tm X /\ member (sred X X) D

ctx_member1 < case H2.
Subgoal 1:

Variables: D H L
IH : forall C D H, ctx C D -> member H C * ->
       (exists X, H = tm X /\ member (sred X X) D)
H1 : ctx (H :: L) D
============================
 exists X, H = tm X /\ member (sred X X) D

Subgoal 2 is:
 exists X, H = tm X /\ member (sred X X) D

ctx_member1 < case H1.
Subgoal 1:

Variables: D1 C1
IH : forall C D H, ctx C D -> member H C * ->
       (exists X, H = tm X /\ member (sred X X) D)
H3 : ctx C1 D1
============================
 exists X, tm n1 = tm X /\ member (sred X X) (sred n1 n1 :: D1)

Subgoal 2 is:
 exists X, H = tm X /\ member (sred X X) D

ctx_member1 < search.
Subgoal 2:

Variables: D H L B
IH : forall C D H, ctx C D -> member H C * ->
       (exists X, H = tm X /\ member (sred X X) D)
H1 : ctx (B :: L) D
H3 : member H L *
============================
 exists X, H = tm X /\ member (sred X X) D

ctx_member1 < case H1.
Subgoal 2:

Variables: H D1 C1
IH : forall C D H, ctx C D -> member H C * ->
       (exists X, H = tm X /\ member (sred X X) D)
H3 : member (H n1) C1 *
H4 : ctx C1 D1
============================
 exists X, H n1 = tm X /\ member (sred X X) (sred n1 n1 :: D1)

ctx_member1 < apply IH to H4 H3.
Subgoal 2:

Variables: D1 C1 X
IH : forall C D H, ctx C D -> member H C * ->
       (exists X, H = tm X /\ member (sred X X) D)
H3 : member (tm (X n1)) C1 *
H4 : ctx C1 D1
H5 : member (sred (X n1) (X n1)) D1
============================
 exists X1, tm (X n1) = tm X1 /\ member (sred X1 X1) (sred n1 n1 :: D1)

ctx_member1 < search.
Proof completed.
Abella < Theorem ctx_member2 : 
forall C D H, ctx C D -> member H D ->
  (exists X, H = sred X X /\ member (tm X) C).


============================
 forall C D H, ctx C D -> member H D ->
   (exists X, H = sred X X /\ member (tm X) C)

ctx_member2 < induction on 2.

IH : forall C D H, ctx C D -> member H D * ->
       (exists X, H = sred X X /\ member (tm X) C)
============================
 forall C D H, ctx C D -> member H D @ ->
   (exists X, H = sred X X /\ member (tm X) C)

ctx_member2 < intros.

Variables: C D H
IH : forall C D H, ctx C D -> member H D * ->
       (exists X, H = sred X X /\ member (tm X) C)
H1 : ctx C D
H2 : member H D @
============================
 exists X, H = sred X X /\ member (tm X) C

ctx_member2 < case H2.
Subgoal 1:

Variables: C H L
IH : forall C D H, ctx C D -> member H D * ->
       (exists X, H = sred X X /\ member (tm X) C)
H1 : ctx C (H :: L)
============================
 exists X, H = sred X X /\ member (tm X) C

Subgoal 2 is:
 exists X, H = sred X X /\ member (tm X) C

ctx_member2 < case H1.
Subgoal 1:

Variables: D1 C1
IH : forall C D H, ctx C D -> member H D * ->
       (exists X, H = sred X X /\ member (tm X) C)
H3 : ctx C1 D1
============================
 exists X, sred n1 n1 = sred X X /\ member (tm X) (tm n1 :: C1)

Subgoal 2 is:
 exists X, H = sred X X /\ member (tm X) C

ctx_member2 < search.
Subgoal 2:

Variables: C H L B
IH : forall C D H, ctx C D -> member H D * ->
       (exists X, H = sred X X /\ member (tm X) C)
H1 : ctx C (B :: L)
H3 : member H L *
============================
 exists X, H = sred X X /\ member (tm X) C

ctx_member2 < case H1.
Subgoal 2:

Variables: H D1 C1
IH : forall C D H, ctx C D -> member H D * ->
       (exists X, H = sred X X /\ member (tm X) C)
H3 : member (H n1) D1 *
H4 : ctx C1 D1
============================
 exists X, H n1 = sred X X /\ member (tm X) (tm n1 :: C1)

ctx_member2 < apply IH to H4 H3.
Subgoal 2:

Variables: D1 C1 X
IH : forall C D H, ctx C D -> member H D * ->
       (exists X, H = sred X X /\ member (tm X) C)
H3 : member (sred (X n1) (X n1)) D1 *
H4 : ctx C1 D1
H5 : member (tm (X n1)) C1
============================
 exists X1, sred (X n1) (X n1) = sred X1 X1 /\ member (tm X1) (tm n1 :: C1)

ctx_member2 < search.
Proof completed.
Abella < Theorem wh_ctx : 
forall C D T T', ctx C D -> {D |- wh T T'} -> {wh T T'}.


============================
 forall C D T T', ctx C D -> {D |- wh T T'} -> {wh T T'}

wh_ctx < induction on 2.

IH : forall C D T T', ctx C D -> {D |- wh T T'}* -> {wh T T'}
============================
 forall C D T T', ctx C D -> {D |- wh T T'}@ -> {wh T T'}

wh_ctx < intros.

Variables: C D T T'
IH : forall C D T T', ctx C D -> {D |- wh T T'}* -> {wh T T'}
H1 : ctx C D
H2 : {D |- wh T T'}@
============================
 {wh T T'}

wh_ctx < case H2.
Subgoal 1:

Variables: C D M R
IH : forall C D T T', ctx C D -> {D |- wh T T'}* -> {wh T T'}
H1 : ctx C D
============================
 {wh (app (abs R) M) (R M)}

Subgoal 2 is:
 {wh (app M N) (app M' N)}

Subgoal 3 is:
 {wh T T'}

wh_ctx < search.
Subgoal 2:

Variables: C D M' M N
IH : forall C D T T', ctx C D -> {D |- wh T T'}* -> {wh T T'}
H1 : ctx C D
H3 : {D |- wh M M'}*
============================
 {wh (app M N) (app M' N)}

Subgoal 3 is:
 {wh T T'}

wh_ctx < apply IH to H1 H3.
Subgoal 2:

Variables: C D M' M N
IH : forall C D T T', ctx C D -> {D |- wh T T'}* -> {wh T T'}
H1 : ctx C D
H3 : {D |- wh M M'}*
H4 : {wh M M'}
============================
 {wh (app M N) (app M' N)}

Subgoal 3 is:
 {wh T T'}

wh_ctx < search.
Subgoal 3:

Variables: C D T T' F
IH : forall C D T T', ctx C D -> {D |- wh T T'}* -> {wh T T'}
H1 : ctx C D
H3 : {D, [F] |- wh T T'}*
H4 : member F D
============================
 {wh T T'}

wh_ctx < apply ctx_member2 to H1 H4.
Subgoal 3:

Variables: C D T T' X
IH : forall C D T T', ctx C D -> {D |- wh T T'}* -> {wh T T'}
H1 : ctx C D
H3 : {D, [sred X X] |- wh T T'}*
H4 : member (sred X X) D
H5 : member (tm X) C
============================
 {wh T T'}

wh_ctx < case H3.
Proof completed.
Abella < Theorem srefl : 
forall C D T, ctx C D -> {C |- tm T} -> {D |- sred T T}.


============================
 forall C D T, ctx C D -> {C |- tm T} -> {D |- sred T T}

srefl < induction on 2.

IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
============================
 forall C D T, ctx C D -> {C |- tm T}@ -> {D |- sred T T}

srefl < intros.

Variables: C D T
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H2 : {C |- tm T}@
============================
 {D |- sred T T}

srefl < case H2.
Subgoal 1:

Variables: C D N M
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H3 : {C |- tm M}*
H4 : {C |- tm N}*
============================
 {D |- sred (app M N) (app M N)}

Subgoal 2 is:
 {D |- sred (abs R) (abs R)}

Subgoal 3 is:
 {D |- sred T T}

srefl < apply IH to H1 H3.
Subgoal 1:

Variables: C D N M
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H3 : {C |- tm M}*
H4 : {C |- tm N}*
H5 : {D |- sred M M}
============================
 {D |- sred (app M N) (app M N)}

Subgoal 2 is:
 {D |- sred (abs R) (abs R)}

Subgoal 3 is:
 {D |- sred T T}

srefl < apply IH to H1 H4.
Subgoal 1:

Variables: C D N M
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H3 : {C |- tm M}*
H4 : {C |- tm N}*
H5 : {D |- sred M M}
H6 : {D |- sred N N}
============================
 {D |- sred (app M N) (app M N)}

Subgoal 2 is:
 {D |- sred (abs R) (abs R)}

Subgoal 3 is:
 {D |- sred T T}

srefl < search.
Subgoal 2:

Variables: C D R
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H3 : {C, tm n1 |- tm (R n1)}*
============================
 {D |- sred (abs R) (abs R)}

Subgoal 3 is:
 {D |- sred T T}

srefl < apply IH to _ H3.
Subgoal 2:

Variables: C D R
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H3 : {C, tm n1 |- tm (R n1)}*
H4 : {D, sred n1 n1 |- sred (R n1) (R n1)}
============================
 {D |- sred (abs R) (abs R)}

Subgoal 3 is:
 {D |- sred T T}

srefl < search.
Subgoal 3:

Variables: C D T F
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H3 : {C, [F] |- tm T}*
H4 : member F C
============================
 {D |- sred T T}

srefl < apply ctx_member1 to H1 H4.
Subgoal 3:

Variables: C D T X
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H3 : {C, [tm X] |- tm T}*
H4 : member (tm X) C
H5 : member (sred X X) D
============================
 {D |- sred T T}

srefl < case H3.
Subgoal 3:

Variables: C D T
IH : forall C D T, ctx C D -> {C |- tm T}* -> {D |- sred T T}
H1 : ctx C D
H4 : member (tm T) C
H5 : member (sred T T) D
============================
 {D |- sred T T}

srefl < search.
Proof completed.
Abella < Theorem ssubst : 
forall C D T T' S S', nabla x, ctx C D ->
  {D, sred x x |- sred (T x) (T' x)} -> {D |- sred S S'} ->
  {D |- sred (T S) (T' S')}.


============================
 forall C D T T' S S', nabla x, ctx C D ->
   {D, sred x x |- sred (T x) (T' x)} -> {D |- sred S S'} ->
   {D |- sred (T S) (T' S')}

ssubst < induction on 2.

IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
============================
 forall C D T T' S S', nabla x, ctx C D ->
   {D, sred x x |- sred (T x) (T' x)}@ -> {D |- sred S S'} ->
   {D |- sred (T S) (T' S')}

ssubst < intros.

Variables: C D T T' S S'
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H2 : {D, sred n1 n1 |- sred (T n1) (T' n1)}@
H3 : {D |- sred S S'}
============================
 {D |- sred (T S) (T' S')}

ssubst < case H2.
Subgoal 1:

Variables: C D T T' S S' M2
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1 |- wh (T n1) (M2 n1)}*
H5 : {D, sred n1 n1 |- sred (M2 n1) (T' n1)}*
============================
 {D |- sred (T S) (T' S')}

Subgoal 2 is:
 {D |- sred (app (M1 S) (N1 S)) (app (M2 S') (N2 S'))}

Subgoal 3 is:
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < apply IH to H1 H5 H3.
Subgoal 1:

Variables: C D T T' S S' M2
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1 |- wh (T n1) (M2 n1)}*
H5 : {D, sred n1 n1 |- sred (M2 n1) (T' n1)}*
H6 : {D |- sred (M2 S) (T' S')}
============================
 {D |- sred (T S) (T' S')}

Subgoal 2 is:
 {D |- sred (app (M1 S) (N1 S)) (app (M2 S') (N2 S'))}

Subgoal 3 is:
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < apply wh_ctx to _ H4.
Subgoal 1:

Variables: C D T T' S S' M2
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1 |- wh (T n1) (M2 n1)}*
H5 : {D, sred n1 n1 |- sred (M2 n1) (T' n1)}*
H6 : {D |- sred (M2 S) (T' S')}
H7 : {wh (T n1) (M2 n1)}
============================
 {D |- sred (T S) (T' S')}

Subgoal 2 is:
 {D |- sred (app (M1 S) (N1 S)) (app (M2 S') (N2 S'))}

Subgoal 3 is:
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst <  inst H7 with n1 = S.
Subgoal 1:

Variables: C D T T' S S' M2
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1 |- wh (T n1) (M2 n1)}*
H5 : {D, sred n1 n1 |- sred (M2 n1) (T' n1)}*
H6 : {D |- sred (M2 S) (T' S')}
H7 : {wh (T n1) (M2 n1)}
H8 : {wh (T S) (M2 S)}
============================
 {D |- sred (T S) (T' S')}

Subgoal 2 is:
 {D |- sred (app (M1 S) (N1 S)) (app (M2 S') (N2 S'))}

Subgoal 3 is:
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < search.
Subgoal 2:

Variables: C D S S' N2 N1 M2 M1
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1 |- sred (M1 n1) (M2 n1)}*
H5 : {D, sred n1 n1 |- sred (N1 n1) (N2 n1)}*
============================
 {D |- sred (app (M1 S) (N1 S)) (app (M2 S') (N2 S'))}

Subgoal 3 is:
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < apply IH to H1 H4 H3.
Subgoal 2:

Variables: C D S S' N2 N1 M2 M1
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1 |- sred (M1 n1) (M2 n1)}*
H5 : {D, sred n1 n1 |- sred (N1 n1) (N2 n1)}*
H6 : {D |- sred (M1 S) (M2 S')}
============================
 {D |- sred (app (M1 S) (N1 S)) (app (M2 S') (N2 S'))}

Subgoal 3 is:
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < apply IH to H1 H5 H3.
Subgoal 2:

Variables: C D S S' N2 N1 M2 M1
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1 |- sred (M1 n1) (M2 n1)}*
H5 : {D, sred n1 n1 |- sred (N1 n1) (N2 n1)}*
H6 : {D |- sred (M1 S) (M2 S')}
H7 : {D |- sred (N1 S) (N2 S')}
============================
 {D |- sred (app (M1 S) (N1 S)) (app (M2 S') (N2 S'))}

Subgoal 3 is:
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < search.
Subgoal 3:

Variables: C D S S' R2 R1
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1, sred n2 n2 |- sred (R1 n1 n2) (R2 n1 n2)}*
============================
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < apply IH to _ H4 H3.
Subgoal 3:

Variables: C D S S' R2 R1
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1, sred n2 n2 |- sred (R1 n1 n2) (R2 n1 n2)}*
H5 : {D, sred n2 n2 |- sred (R1 S n2) (R2 S' n2)}
============================
 {D |- sred (abs (R1 S)) (abs (R2 S'))}

Subgoal 4 is:
 {D |- sred (T S) (T' S')}

ssubst < search.
Subgoal 4:

Variables: C D T T' S S' F
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1, [F n1] |- sred (T n1) (T' n1)}*
H5 : member (F n1) (sred n1 n1 :: D)
============================
 {D |- sred (T S) (T' S')}

ssubst < case H5.
Subgoal 4.1:

Variables: C D T T' S S'
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1, [sred n1 n1] |- sred (T n1) (T' n1)}*
============================
 {D |- sred (T S) (T' S')}

Subgoal 4.2 is:
 {D |- sred (T S) (T' S')}

ssubst < case H4.
Subgoal 4.1:

Variables: C D S S'
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
============================
 {D |- sred S S'}

Subgoal 4.2 is:
 {D |- sred (T S) (T' S')}

ssubst < search.
Subgoal 4.2:

Variables: C D T T' S S' F
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1, [F n1] |- sred (T n1) (T' n1)}*
H6 : member (F n1) D
============================
 {D |- sred (T S) (T' S')}

ssubst < apply ctx_member2 to H1 H6.
Subgoal 4.2:

Variables: C D T T' S S' X
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H4 : {D, sred n1 n1, [sred (X n1) (X n1)] |- sred (T n1) (T' n1)}*
H6 : member (sred (X n1) (X n1)) D
H7 : member (tm (X n1)) C
============================
 {D |- sred (T S) (T' S')}

ssubst < case H4.
Subgoal 4.2:

Variables: C D T' S S'
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H6 : member (sred (T' n1) (T' n1)) D
H7 : member (tm (T' n1)) C
============================
 {D |- sred (T' S) (T' S')}

ssubst < apply member_prune to H6.
Subgoal 4.2:

Variables: C D S S' F2
IH : forall C D T T' S S', nabla x, ctx C D ->
       {D, sred x x |- sred (T x) (T' x)}* -> {D |- sred S S'} ->
       {D |- sred (T S) (T' S')}
H1 : ctx C D
H3 : {D |- sred S S'}
H6 : member (sred F2 F2) D
H7 : member (tm F2) C
============================
 {D |- sred F2 F2}

ssubst < search.
Proof completed.
Abella < Theorem name_not_beta : 
forall T, nabla x, {beta x T} -> false.


============================
 forall T, nabla x, {beta x T} -> false

name_not_beta < intros.

Variables: T
H1 : {beta n1 T}
============================
 false

name_not_beta < case H1.
Proof completed.
Abella < Theorem var_not_beta : 
forall C D T T', ctx C D -> member (tm T) C -> {beta T T'} -> false.


============================
 forall C D T T', ctx C D -> member (tm T) C -> {beta T T'} -> false

var_not_beta < induction on 2.

IH : forall C D T T', ctx C D -> member (tm T) C * -> {beta T T'} -> false
============================
 forall C D T T', ctx C D -> member (tm T) C @ -> {beta T T'} -> false

var_not_beta < intros.

Variables: C D T T'
IH : forall C D T T', ctx C D -> member (tm T) C * -> {beta T T'} -> false
H1 : ctx C D
H2 : member (tm T) C @
H3 : {beta T T'}
============================
 false

var_not_beta < case H2.
Subgoal 1:

Variables: D T T' L
IH : forall C D T T', ctx C D -> member (tm T) C * -> {beta T T'} -> false
H1 : ctx (tm T :: L) D
H3 : {beta T T'}
============================
 false

Subgoal 2 is:
 false

var_not_beta < case H1.
Subgoal 1:

Variables: T' D1 C1
IH : forall C D T T', ctx C D -> member (tm T) C * -> {beta T T'} -> false
H3 : {beta n1 (T' n1)}
H4 : ctx C1 D1
============================
 false

Subgoal 2 is:
 false

var_not_beta < case H3.
Subgoal 2:

Variables: D T T' L B
IH : forall C D T T', ctx C D -> member (tm T) C * -> {beta T T'} -> false
H1 : ctx (B :: L) D
H3 : {beta T T'}
H4 : member (tm T) L *
============================
 false

var_not_beta < case H1.
Subgoal 2:

Variables: T T' D1 C1
IH : forall C D T T', ctx C D -> member (tm T) C * -> {beta T T'} -> false
H3 : {beta (T n1) (T' n1)}
H4 : member (tm (T n1)) C1 *
H5 : ctx C1 D1
============================
 false

var_not_beta < apply IH to H5 H4 H3.
Proof completed.
Abella < Theorem var_not_abs : 
forall C D R, ctx C D -> member (tm (abs R)) C -> false.


============================
 forall C D R, ctx C D -> member (tm (abs R)) C -> false

var_not_abs < induction on 2.

IH : forall C D R, ctx C D -> member (tm (abs R)) C * -> false
============================
 forall C D R, ctx C D -> member (tm (abs R)) C @ -> false

var_not_abs < intros.

Variables: C D R
IH : forall C D R, ctx C D -> member (tm (abs R)) C * -> false
H1 : ctx C D
H2 : member (tm (abs R)) C @
============================
 false

var_not_abs < case H2.
Subgoal 1:

Variables: D R L
IH : forall C D R, ctx C D -> member (tm (abs R)) C * -> false
H1 : ctx (tm (abs R) :: L) D
============================
 false

Subgoal 2 is:
 false

var_not_abs < case H1.
Subgoal 2:

Variables: D R L B
IH : forall C D R, ctx C D -> member (tm (abs R)) C * -> false
H1 : ctx (B :: L) D
H3 : member (tm (abs R)) L *
============================
 false

var_not_abs < case H1.
Subgoal 2:

Variables: R D1 C1
IH : forall C D R, ctx C D -> member (tm (abs R)) C * -> false
H3 : member (tm (abs (R n1))) C1 *
H4 : ctx C1 D1
============================
 false

var_not_abs < apply IH to H4 H3.
Proof completed.
Abella < Theorem sred_beta : 
forall C D M N N' R, ctx C D -> {D |- sred M (abs R)} -> {D |- sred N N'} ->
  {D |- sred (app M N) (R N')}.


============================
 forall C D M N N' R, ctx C D -> {D |- sred M (abs R)} -> {D |- sred N N'} ->
   {D |- sred (app M N) (R N')}

sred_beta < induction on 2.

IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
============================
 forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}@ ->
   {D |- sred N N'} -> {D |- sred (app M N) (R N')}

sred_beta < intros.

Variables: C D M N N' R
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H2 : {D |- sred M (abs R)}@
H3 : {D |- sred N N'}
============================
 {D |- sred (app M N) (R N')}

sred_beta < case H2.
Subgoal 1:

Variables: C D M N N' R M2
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H3 : {D |- sred N N'}
H4 : {D |- wh M M2}*
H5 : {D |- sred M2 (abs R)}*
============================
 {D |- sred (app M N) (R N')}

Subgoal 2 is:
 {D |- sred (app (abs R1) N) (R N')}

Subgoal 3 is:
 {D |- sred (app M N) (R N')}

sred_beta < apply IH to H1 H5 H3.
Subgoal 1:

Variables: C D M N N' R M2
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H3 : {D |- sred N N'}
H4 : {D |- wh M M2}*
H5 : {D |- sred M2 (abs R)}*
H6 : {D |- sred (app M2 N) (R N')}
============================
 {D |- sred (app M N) (R N')}

Subgoal 2 is:
 {D |- sred (app (abs R1) N) (R N')}

Subgoal 3 is:
 {D |- sred (app M N) (R N')}

sred_beta < search.
Subgoal 2:

Variables: C D N N' R R1
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H3 : {D |- sred N N'}
H4 : {D, sred n1 n1 |- sred (R1 n1) (R n1)}*
============================
 {D |- sred (app (abs R1) N) (R N')}

Subgoal 3 is:
 {D |- sred (app M N) (R N')}

sred_beta < apply ssubst to H1 H4 H3.
Subgoal 2:

Variables: C D N N' R R1
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H3 : {D |- sred N N'}
H4 : {D, sred n1 n1 |- sred (R1 n1) (R n1)}*
H5 : {D |- sred (R1 N) (R N')}
============================
 {D |- sred (app (abs R1) N) (R N')}

Subgoal 3 is:
 {D |- sred (app M N) (R N')}

sred_beta < search.
Subgoal 3:

Variables: C D M N N' R F
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H3 : {D |- sred N N'}
H4 : {D, [F] |- sred M (abs R)}*
H5 : member F D
============================
 {D |- sred (app M N) (R N')}

sred_beta < apply ctx_member2 to H1 H5.
Subgoal 3:

Variables: C D M N N' R X
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H3 : {D |- sred N N'}
H4 : {D, [sred X X] |- sred M (abs R)}*
H5 : member (sred X X) D
H6 : member (tm X) C
============================
 {D |- sred (app M N) (R N')}

sred_beta < case H4.
Subgoal 3:

Variables: C D N N' R
IH : forall C D M N N' R, ctx C D -> {D |- sred M (abs R)}* ->
       {D |- sred N N'} -> {D |- sred (app M N) (R N')}
H1 : ctx C D
H3 : {D |- sred N N'}
H5 : member (sred (abs R) (abs R)) D
H6 : member (tm (abs R)) C
============================
 {D |- sred (app (abs R) N) (R N')}

sred_beta < apply var_not_abs to H1 H6.
Proof completed.
Abella < Theorem sappend : 
forall C D T T' T'', ctx C D -> {D |- sred T T'} -> {beta T' T''} ->
  {D |- sred T T''}.


============================
 forall C D T T' T'', ctx C D -> {D |- sred T T'} -> {beta T' T''} ->
   {D |- sred T T''}

sappend < induction on 2.

IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
============================
 forall C D T T' T'', ctx C D -> {D |- sred T T'}@ -> {beta T' T''} ->
   {D |- sred T T''}

sappend < intros.

Variables: C D T T' T''
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H2 : {D |- sred T T'}@
H3 : {beta T' T''}
============================
 {D |- sred T T''}

sappend < case H2.
Subgoal 1:

Variables: C D T T' T'' M2
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H3 : {beta T' T''}
H4 : {D |- wh T M2}*
H5 : {D |- sred M2 T'}*
============================
 {D |- sred T T''}

Subgoal 2 is:
 {D |- sred (app M1 N1) T''}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < apply IH to H1 H5 H3.
Subgoal 1:

Variables: C D T T' T'' M2
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H3 : {beta T' T''}
H4 : {D |- wh T M2}*
H5 : {D |- sred M2 T'}*
H6 : {D |- sred M2 T''}
============================
 {D |- sred T T''}

Subgoal 2 is:
 {D |- sred (app M1 N1) T''}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < search.
Subgoal 2:

Variables: C D T'' N2 N1 M2 M1
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H3 : {beta (app M2 N2) T''}
H4 : {D |- sred M1 M2}*
H5 : {D |- sred N1 N2}*
============================
 {D |- sred (app M1 N1) T''}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < case H3.
Subgoal 2.1:

Variables: C D N2 N1 M2 M1 M'
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D |- sred M1 M2}*
H5 : {D |- sred N1 N2}*
H6 : {beta M2 M'}
============================
 {D |- sred (app M1 N1) (app M' N2)}

Subgoal 2.2 is:
 {D |- sred (app M1 N1) (app M2 N')}

Subgoal 2.3 is:
 {D |- sred (app M1 N1) (R N2)}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < apply IH to H1 H4 H6.
Subgoal 2.1:

Variables: C D N2 N1 M2 M1 M'
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D |- sred M1 M2}*
H5 : {D |- sred N1 N2}*
H6 : {beta M2 M'}
H7 : {D |- sred M1 M'}
============================
 {D |- sred (app M1 N1) (app M' N2)}

Subgoal 2.2 is:
 {D |- sred (app M1 N1) (app M2 N')}

Subgoal 2.3 is:
 {D |- sred (app M1 N1) (R N2)}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < search.
Subgoal 2.2:

Variables: C D N2 N1 M2 M1 N'
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D |- sred M1 M2}*
H5 : {D |- sred N1 N2}*
H6 : {beta N2 N'}
============================
 {D |- sred (app M1 N1) (app M2 N')}

Subgoal 2.3 is:
 {D |- sred (app M1 N1) (R N2)}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < apply IH to H1 H5 H6.
Subgoal 2.2:

Variables: C D N2 N1 M2 M1 N'
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D |- sred M1 M2}*
H5 : {D |- sred N1 N2}*
H6 : {beta N2 N'}
H7 : {D |- sred N1 N'}
============================
 {D |- sred (app M1 N1) (app M2 N')}

Subgoal 2.3 is:
 {D |- sred (app M1 N1) (R N2)}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < search.
Subgoal 2.3:

Variables: C D N2 N1 M1 R
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D |- sred M1 (abs R)}*
H5 : {D |- sred N1 N2}*
============================
 {D |- sred (app M1 N1) (R N2)}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < apply sred_beta to H1 H4 H5.
Subgoal 2.3:

Variables: C D N2 N1 M1 R
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D |- sred M1 (abs R)}*
H5 : {D |- sred N1 N2}*
H6 : {D |- sred (app M1 N1) (R N2)}
============================
 {D |- sred (app M1 N1) (R N2)}

Subgoal 3 is:
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < search.
Subgoal 3:

Variables: C D T'' R2 R1
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H3 : {beta (abs R2) T''}
H4 : {D, sred n1 n1 |- sred (R1 n1) (R2 n1)}*
============================
 {D |- sred (abs R1) T''}

Subgoal 4 is:
 {D |- sred T T''}

sappend < case H3.
Subgoal 3:

Variables: C D R2 R1 S2
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D, sred n1 n1 |- sred (R1 n1) (R2 n1)}*
H5 : {beta (R2 n1) (S2 n1)}
============================
 {D |- sred (abs R1) (abs S2)}

Subgoal 4 is:
 {D |- sred T T''}

sappend < apply IH to _ H4 H5.
Subgoal 3:

Variables: C D R2 R1 S2
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H4 : {D, sred n1 n1 |- sred (R1 n1) (R2 n1)}*
H5 : {beta (R2 n1) (S2 n1)}
H6 : {D, sred n1 n1 |- sred (R1 n1) (S2 n1)}
============================
 {D |- sred (abs R1) (abs S2)}

Subgoal 4 is:
 {D |- sred T T''}

sappend < search.
Subgoal 4:

Variables: C D T T' T'' F
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H3 : {beta T' T''}
H4 : {D, [F] |- sred T T'}*
H5 : member F D
============================
 {D |- sred T T''}

sappend < apply ctx_member2 to H1 H5.
Subgoal 4:

Variables: C D T T' T'' X
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H3 : {beta T' T''}
H4 : {D, [sred X X] |- sred T T'}*
H5 : member (sred X X) D
H6 : member (tm X) C
============================
 {D |- sred T T''}

sappend < case H4.
Subgoal 4:

Variables: C D T' T''
IH : forall C D T T' T'', ctx C D -> {D |- sred T T'}* -> {beta T' T''} ->
       {D |- sred T T''}
H1 : ctx C D
H3 : {beta T' T''}
H5 : member (sred T' T') D
H6 : member (tm T') C
============================
 {D |- sred T' T''}

sappend < apply var_not_beta to H1 H6 H3.
Proof completed.
Abella < Theorem standardization : 
forall T T', {tm T} -> {betas T T'} -> {sred T T'}.


============================
 forall T T', {tm T} -> {betas T T'} -> {sred T T'}

standardization < induction on 2.

IH : forall T T', {tm T} -> {betas T T'}* -> {sred T T'}
============================
 forall T T', {tm T} -> {betas T T'}@ -> {sred T T'}

standardization < intros.

Variables: T T'
IH : forall T T', {tm T} -> {betas T T'}* -> {sred T T'}
H1 : {tm T}
H2 : {betas T T'}@
============================
 {sred T T'}

standardization < case H2.
Subgoal 1:

Variables: T'
IH : forall T T', {tm T} -> {betas T T'}* -> {sred T T'}
H1 : {tm T'}
============================
 {sred T' T'}

Subgoal 2 is:
 {sred T T'}

standardization < apply srefl to _ H1.
Subgoal 1:

Variables: T'
IH : forall T T', {tm T} -> {betas T T'}* -> {sred T T'}
H1 : {tm T'}
H3 : {sred T' T'}
============================
 {sred T' T'}

Subgoal 2 is:
 {sred T T'}

standardization < search.
Subgoal 2:

Variables: T T' P
IH : forall T T', {tm T} -> {betas T T'}* -> {sred T T'}
H1 : {tm T}
H3 : {betas T P}*
H4 : {beta P T'}*
============================
 {sred T T'}

standardization < apply IH to H1 H3.
Subgoal 2:

Variables: T T' P
IH : forall T T', {tm T} -> {betas T T'}* -> {sred T T'}
H1 : {tm T}
H3 : {betas T P}*
H4 : {beta P T'}*
H5 : {sred T P}
============================
 {sred T T'}

standardization < apply sappend to _ H5 H4.
Subgoal 2:

Variables: T T' P
IH : forall T T', {tm T} -> {betas T T'}* -> {sred T T'}
H1 : {tm T}
H3 : {betas T P}*
H4 : {beta P T'}*
H5 : {sred T P}
H6 : {sred T T'}
============================
 {sred T T'}

standardization < search.
Proof completed.
Abella <