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

Abella < Close natural, typ, exp.

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


============================
 forall G E, nabla x, member (E x) G -> (exists E', E = y\E')

member_prune < induction on 1.

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

member_prune < intros.

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

member_prune < case H1.
Subgoal 1:

Variables: G2 G1
IH : forall G E, nabla x, member (E x) G * -> (exists E', E = y\E')
============================
 exists E', z1\G1 = y\E'

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

member_prune < search.
Subgoal 2:

Variables: E G2 G1
IH : forall G E, nabla x, member (E x) G * -> (exists E', E = y\E')
H2 : member (E n1) G2 *
============================
 exists E', E = y\E'

member_prune < apply IH to H2.
Subgoal 2:

Variables: G2 G1 E'
IH : forall G E, nabla x, member (E x) G * -> (exists E', E = y\E')
H2 : member E' G2 *
============================
 exists E'1, z1\E' = y\E'1

member_prune < search.
Proof completed.
Abella < Define insert : o -> olist -> olist -> prop by 
insert E L (E :: L);
insert E (F :: L) (F :: L') := insert E L L'.

Abella < Theorem member_insert : 
forall E1 E2 L L', insert E1 L L' -> member E2 L' -> E1 = E2 \/ member E2 L.


============================
 forall E1 E2 L L', insert E1 L L' -> member E2 L' -> E1 = E2 \/ member E2 L

member_insert < induction on 1.

IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
============================
 forall E1 E2 L L', insert E1 L L' @ -> member E2 L' -> E1 = E2 \/
   member E2 L

member_insert < intros.

Variables: E1 E2 L L'
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H1 : insert E1 L L' @
H2 : member E2 L'
============================
 E1 = E2 \/ member E2 L

member_insert < case H1.
Subgoal 1:

Variables: E1 E2 L
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H2 : member E2 (E1 :: L)
============================
 E1 = E2 \/ member E2 L

Subgoal 2 is:
 E1 = E2 \/ member E2 (F :: L1)

member_insert < case H2.
Subgoal 1.1:

Variables: E1 L
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
============================
 E1 = E1 \/ member E1 L

Subgoal 1.2 is:
 E1 = E2 \/ member E2 L

Subgoal 2 is:
 E1 = E2 \/ member E2 (F :: L1)

member_insert < search.
Subgoal 1.2:

Variables: E1 E2 L
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H3 : member E2 L
============================
 E1 = E2 \/ member E2 L

Subgoal 2 is:
 E1 = E2 \/ member E2 (F :: L1)

member_insert < search.
Subgoal 2:

Variables: E1 E2 L'1 F L1
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H2 : member E2 (F :: L'1)
H3 : insert E1 L1 L'1 *
============================
 E1 = E2 \/ member E2 (F :: L1)

member_insert < case H2.
Subgoal 2.1:

Variables: E1 L'1 F L1
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H3 : insert E1 L1 L'1 *
============================
 E1 = F \/ member F (F :: L1)

Subgoal 2.2 is:
 E1 = E2 \/ member E2 (F :: L1)

member_insert < search.
Subgoal 2.2:

Variables: E1 E2 L'1 F L1
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H3 : insert E1 L1 L'1 *
H4 : member E2 L'1
============================
 E1 = E2 \/ member E2 (F :: L1)

member_insert < apply IH to H3 H4.
Subgoal 2.2:

Variables: E1 E2 L'1 F L1
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H3 : insert E1 L1 L'1 *
H4 : member E2 L'1
H5 : E1 = E2 \/ member E2 L1
============================
 E1 = E2 \/ member E2 (F :: L1)

member_insert < case H5.
Subgoal 2.2.1:

Variables: E2 L'1 F L1
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H3 : insert E2 L1 L'1 *
H4 : member E2 L'1
============================
 E2 = E2 \/ member E2 (F :: L1)

Subgoal 2.2.2 is:
 E1 = E2 \/ member E2 (F :: L1)

member_insert < search.
Subgoal 2.2.2:

Variables: E1 E2 L'1 F L1
IH : forall E1 E2 L L', insert E1 L L' * -> member E2 L' -> E1 = E2 \/
       member E2 L
H3 : insert E1 L1 L'1 *
H4 : member E2 L'1
H6 : member E2 L1
============================
 E1 = E2 \/ member E2 (F :: L1)

member_insert < search.
Proof completed.
Abella < Theorem insert_prune : 
forall E L1 L2, nabla x, insert (E x) (L1 x) L2 ->
  (exists E' L1', E = x\E' /\ L1 = x\L1').


============================
 forall E L1 L2, nabla x, insert (E x) (L1 x) L2 ->
   (exists E' L1', E = x\E' /\ L1 = x\L1')

insert_prune < induction on 1.

IH : forall E L1 L2, nabla x, insert (E x) (L1 x) L2 * ->
       (exists E' L1', E = x\E' /\ L1 = x\L1')
============================
 forall E L1 L2, nabla x, insert (E x) (L1 x) L2 @ ->
   (exists E' L1', E = x\E' /\ L1 = x\L1')

insert_prune < intros.

Variables: E L1 L2
IH : forall E L1 L2, nabla x, insert (E x) (L1 x) L2 * ->
       (exists E' L1', E = x\E' /\ L1 = x\L1')
H1 : insert (E n1) (L1 n1) L2 @
============================
 exists E' L1', E = x\E' /\ L1 = x\L1'

insert_prune < case H1.
Subgoal 1:

Variables: L4 L3
IH : forall E L1 L2, nabla x, insert (E x) (L1 x) L2 * ->
       (exists E' L1', E = x\E' /\ L1 = x\L1')
============================
 exists E' L1', z1\L3 = x\E' /\ z1\L4 = x\L1'

Subgoal 2 is:
 exists E' L1', E = x\E' /\ z1\L3 :: L z1 = x\L1'

insert_prune < search.
Subgoal 2:

Variables: E L4 L3 L
IH : forall E L1 L2, nabla x, insert (E x) (L1 x) L2 * ->
       (exists E' L1', E = x\E' /\ L1 = x\L1')
H2 : insert (E n1) (L n1) L4 *
============================
 exists E' L1', E = x\E' /\ z1\L3 :: L z1 = x\L1'

insert_prune < apply IH to H2.
Subgoal 2:

Variables: L4 L3 E' L1'
IH : forall E L1 L2, nabla x, insert (E x) (L1 x) L2 * ->
       (exists E' L1', E = x\E' /\ L1 = x\L1')
H2 : insert E' L1' L4 *
============================
 exists E'1 L1'1, z1\E' = x\E'1 /\ z1\L3 :: L1' = x\L1'1

insert_prune < search.
Proof completed.
Abella < Theorem sum_type : 
forall N1 N2 N, {sum N1 N2 N} -> {natural N1} /\ {natural N2} /\ {natural N}.


============================
 forall N1 N2 N, {sum N1 N2 N} -> {natural N1} /\ {natural N2} /\ {natural N}

sum_type < induction on 1.

IH : forall N1 N2 N, {sum N1 N2 N}* -> {natural N1} /\ {natural N2} /\
       {natural N}
============================
 forall N1 N2 N, {sum N1 N2 N}@ -> {natural N1} /\ {natural N2} /\
   {natural N}

sum_type < intros.

Variables: N1 N2 N
IH : forall N1 N2 N, {sum N1 N2 N}* -> {natural N1} /\ {natural N2} /\
       {natural N}
H1 : {sum N1 N2 N}@
============================
 {natural N1} /\ {natural N2} /\ {natural N}

sum_type < case H1.
Subgoal 1:

Variables: N
IH : forall N1 N2 N, {sum N1 N2 N}* -> {natural N1} /\ {natural N2} /\
       {natural N}
H2 : {natural N}*
============================
 {natural z} /\ {natural N} /\ {natural N}

Subgoal 2 is:
 {natural (s N5)} /\ {natural N2} /\ {natural (s N3)}

sum_type < search.
Subgoal 2:

Variables: N2 N3 N5
IH : forall N1 N2 N, {sum N1 N2 N}* -> {natural N1} /\ {natural N2} /\
       {natural N}
H2 : {sum N5 N2 N3}*
============================
 {natural (s N5)} /\ {natural N2} /\ {natural (s N3)}

sum_type < apply IH to H2.
Subgoal 2:

Variables: N2 N3 N5
IH : forall N1 N2 N, {sum N1 N2 N}* -> {natural N1} /\ {natural N2} /\
       {natural N}
H2 : {sum N5 N2 N3}*
H3 : {natural N5}
H4 : {natural N2}
H5 : {natural N3}
============================
 {natural (s N5)} /\ {natural N2} /\ {natural (s N3)}

sum_type < search.
Proof completed.
Abella < Define vals : olist -> prop by 
vals nil;
nabla x, vals (val x :: H) := vals H.

Abella < Theorem insert_vals : 
forall E H H', insert E H H' -> vals H' -> vals H.


============================
 forall E H H', insert E H H' -> vals H' -> vals H

insert_vals < induction on 1.

IH : forall E H H', insert E H H' * -> vals H' -> vals H
============================
 forall E H H', insert E H H' @ -> vals H' -> vals H

insert_vals < intros.

Variables: E H H'
IH : forall E H H', insert E H H' * -> vals H' -> vals H
H1 : insert E H H' @
H2 : vals H'
============================
 vals H

insert_vals < case H1.
Subgoal 1:

Variables: E H
IH : forall E H H', insert E H H' * -> vals H' -> vals H
H2 : vals (E :: H)
============================
 vals H

Subgoal 2 is:
 vals (F :: L)

insert_vals < case H2.
Subgoal 1:

Variables: H1
IH : forall E H H', insert E H H' * -> vals H' -> vals H
H3 : vals H1
============================
 vals H1

Subgoal 2 is:
 vals (F :: L)

insert_vals < search.
Subgoal 2:

Variables: E L' F L
IH : forall E H H', insert E H H' * -> vals H' -> vals H
H2 : vals (F :: L')
H3 : insert E L L' *
============================
 vals (F :: L)

insert_vals < case H2.
Subgoal 2:

Variables: E L H1
IH : forall E H H', insert E H H' * -> vals H' -> vals H
H3 : insert (E n1) (L n1) H1 *
H4 : vals H1
============================
 vals (val n1 :: L n1)

insert_vals < apply insert_prune to H3.
Subgoal 2:

Variables: H1 E' L1'
IH : forall E H H', insert E H H' * -> vals H' -> vals H
H3 : insert E' L1' H1 *
H4 : vals H1
============================
 vals (val n1 :: L1')

insert_vals < apply IH to H3 H4.
Subgoal 2:

Variables: H1 E' L1'
IH : forall E H H', insert E H H' * -> vals H' -> vals H
H3 : insert E' L1' H1 *
H4 : vals H1
H5 : vals L1'
============================
 vals (val n1 :: L1')

insert_vals < search.
Proof completed.
Abella < Kind sexp type.

Abella < Type rep exp -> sexp -> o.

Abella < Type sb olist -> exp -> sexp.

Abella < Define sexp : olist -> sexp -> prop,	
sub : olist -> prop,	
xval : sexp -> prop by 
nabla x, sexp (H x) (sb (S x) x) := nabla x, vals (H x) /\ sub (S x) /\ member (val x) (H x);
nabla x, sexp (H x) (sb (S x) x) := nabla x, vals (H x) /\ sub (S x) /\ (exists V, member (rep x V) (S x));
sexp H (sb S (num N)) := vals H /\ sub S /\ {natural N};
sexp H (sb S (plus E1 E2)) := sexp H (sb S E1) /\ sexp H (sb S E2);
sexp H (sb S (lam T1 E2)) := {typ T1} /\ (nabla x, sexp (val x :: H) (sb S (E2 x)));
sexp H (sb S (app E1 E2)) := sexp H (sb S E1) /\ sexp H (sb S E2);
sub nil;
nabla x, sub (rep x V :: S) := xval V /\ sub S;
xval (sb nil (num N)) := {natural N};
xval (sb S (lam T1 E2)) := sexp nil (sb S (lam T1 E2)).

Abella < Theorem sexp_type : 
forall H E', sexp H E' -> (exists S E, E' = sb S E /\ vals H /\ sub S).


============================
 forall H E', sexp H E' -> (exists S E, E' = sb S E /\ vals H /\ sub S)

sexp_type < induction on 1.

IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
============================
 forall H E', sexp H E' @ -> (exists S E, E' = sb S E /\ vals H /\ sub S)

sexp_type < intros.

Variables: H E'
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H1 : sexp H E' @
============================
 exists S E, E' = sb S E /\ vals H /\ sub S

sexp_type < case H1.
Subgoal 1:

Variables: H S
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : vals (H n1)
H3 : sub (S n1) *
H4 : member (val n1) (H n1)
============================
 exists S1 E, sb (S n1) n1 = sb S1 E /\ vals (H n1) /\ sub S1

Subgoal 2 is:
 exists S1 E, sb (S n1) n1 = sb S1 E /\ vals (H n1) /\ sub S1

Subgoal 3 is:
 exists S1 E, sb S (num N) = sb S1 E /\ vals H /\ sub S1

Subgoal 4 is:
 exists S1 E, sb S (plus E1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 5 is:
 exists S1 E, sb S (lam T1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < search.
Subgoal 2:

Variables: H V S
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : vals (H n1)
H3 : sub (S n1) *
H4 : member (rep n1 (V n1)) (S n1)
============================
 exists S1 E, sb (S n1) n1 = sb S1 E /\ vals (H n1) /\ sub S1

Subgoal 3 is:
 exists S1 E, sb S (num N) = sb S1 E /\ vals H /\ sub S1

Subgoal 4 is:
 exists S1 E, sb S (plus E1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 5 is:
 exists S1 E, sb S (lam T1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < search.
Subgoal 3:

Variables: H N S
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : vals H
H3 : sub S *
H4 : {natural N}
============================
 exists S1 E, sb S (num N) = sb S1 E /\ vals H /\ sub S1

Subgoal 4 is:
 exists S1 E, sb S (plus E1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 5 is:
 exists S1 E, sb S (lam T1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < search.
Subgoal 4:

Variables: H E2 E1 S
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : sexp H (sb S E1) *
H3 : sexp H (sb S E2) *
============================
 exists S1 E, sb S (plus E1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 5 is:
 exists S1 E, sb S (lam T1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < apply IH to H2.
Subgoal 4:

Variables: H E2 S1 E
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : sexp H (sb S1 E) *
H3 : sexp H (sb S1 E2) *
H4 : vals H
H5 : sub S1
============================
 exists S2 E1, sb S1 (plus E E2) = sb S2 E1 /\ vals H /\ sub S2

Subgoal 5 is:
 exists S1 E, sb S (lam T1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < search.
Subgoal 5:

Variables: H E2 T1 S
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : {typ T1}
H3 : sexp (val n1 :: H) (sb S (E2 n1)) *
============================
 exists S1 E, sb S (lam T1 E2) = sb S1 E /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < apply IH to H3.
Subgoal 5:

Variables: H T1 S E
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : {typ T1}
H3 : sexp (val n1 :: H) (sb S (E n1)) *
H4 : vals (val n1 :: H)
H5 : sub S
============================
 exists S1 E1, sb S (lam T1 (z1\E z1)) = sb S1 E1 /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < case H4.
Subgoal 5:

Variables: H T1 S E
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : {typ T1}
H3 : sexp (val n1 :: H) (sb S (E n1)) *
H5 : sub S
H6 : vals H
============================
 exists S1 E1, sb S (lam T1 (z1\E z1)) = sb S1 E1 /\ vals H /\ sub S1

Subgoal 6 is:
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < search.
Subgoal 6:

Variables: H E2 E1 S
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : sexp H (sb S E1) *
H3 : sexp H (sb S E2) *
============================
 exists S1 E, sb S (app E1 E2) = sb S1 E /\ vals H /\ sub S1

sexp_type < apply IH to H2.
Subgoal 6:

Variables: H E2 S1 E
IH : forall H E', sexp H E' * -> (exists S E, E' = sb S E /\ vals H /\ sub S)
H2 : sexp H (sb S1 E) *
H3 : sexp H (sb S1 E2) *
H4 : vals H
H5 : sub S1
============================
 exists S2 E1, sb S1 (app E E2) = sb S2 E1 /\ vals H /\ sub S2

sexp_type < search.
Proof completed.
Abella < Theorem sexp_abs : 
forall H H' S E V, nabla x, insert (val x) H' (H x) ->
  sexp (H x) (sb S (E x)) -> xval V -> sexp H' (sb (rep x V :: S) (E x)).


============================
 forall H H' S E V, nabla x, insert (val x) H' (H x) ->
   sexp (H x) (sb S (E x)) -> xval V -> sexp H' (sb (rep x V :: S) (E x))

sexp_abs < induction on 2.

IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
============================
 forall H H' S E V, nabla x, insert (val x) H' (H x) ->
   sexp (H x) (sb S (E x)) @ -> xval V -> sexp H' (sb (rep x V :: S) (E x))

sexp_abs < intros.

Variables: H H' S E V
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S (E n1)) @
H3 : xval V
============================
 sexp H' (sb (rep n1 V :: S) (E n1))

sexp_abs < case H2.
Subgoal 1:

Variables: H H' S V
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) (H' n2) (H n2 n1)
H3 : xval (V n2)
H4 : vals (H n2 n1)
H5 : sub (S n2) *
H6 : member (val n2) (H n2 n1)
============================
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 2 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 3 is:
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply member_insert to H1 H6.
Subgoal 1:

Variables: H H' S V
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) (H' n2) (H n2 n1)
H3 : xval (V n2)
H4 : vals (H n2 n1)
H5 : sub (S n2) *
H6 : member (val n2) (H n2 n1)
H7 : val n1 = val n2 \/ member (val n2) (H' n2)
============================
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 2 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 3 is:
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < case H7.
Subgoal 1:

Variables: H H' S V
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) (H' n2) (H n2 n1)
H3 : xval (V n2)
H4 : vals (H n2 n1)
H5 : sub (S n2) *
H6 : member (val n2) (H n2 n1)
H8 : member (val n2) (H' n2)
============================
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 2 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 3 is:
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply insert_vals to H1 H4.
Subgoal 1:

Variables: H H' S V
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) (H' n2) (H n2 n1)
H3 : xval (V n2)
H4 : vals (H n2 n1)
H5 : sub (S n2) *
H6 : member (val n2) (H n2 n1)
H8 : member (val n2) (H' n2)
H9 : vals (H' n2)
============================
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 2 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 3 is:
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < search.
Subgoal 2:

Variables: H H' S V
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : vals (H n1)
H5 : sub S *
H6 : member (val n1) (H n1)
============================
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 3 is:
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply insert_vals to H1 H4.
Subgoal 2:

Variables: H H' S V
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : vals (H n1)
H5 : sub S *
H6 : member (val n1) (H n1)
H7 : vals H'
============================
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 3 is:
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < search.
Subgoal 3:

Variables: H H' S V V1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) (H' n2) (H n2 n1)
H3 : xval (V n2)
H4 : vals (H n2 n1)
H5 : sub (S n2) *
H6 : member (rep n2 (V1 n2)) (S n2)
============================
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply insert_vals to H1 H4.
Subgoal 3:

Variables: H H' S V V1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) (H' n2) (H n2 n1)
H3 : xval (V n2)
H4 : vals (H n2 n1)
H5 : sub (S n2) *
H6 : member (rep n2 (V1 n2)) (S n2)
H7 : vals (H' n2)
============================
 sexp (H' n2) (sb (rep n1 (V n2) :: S n2) n2)

Subgoal 4 is:
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < search.
Subgoal 4:

Variables: H H' S V V1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : vals (H n1)
H5 : sub S *
H6 : member (rep n1 (V1 n1)) S
============================
 sexp H' (sb (rep n1 V :: S) n1)

Subgoal 5 is:
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply member_prune to H6.
Subgoal 5:

Variables: H H' S V N
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : vals (H n1)
H5 : sub S *
H6 : {natural N}
============================
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply insert_vals to H1 H4.
Subgoal 5:

Variables: H H' S V N
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : vals (H n1)
H5 : sub S *
H6 : {natural N}
H7 : vals H'
============================
 sexp H' (sb (rep n1 V :: S) (num N))

Subgoal 6 is:
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < search.
Subgoal 6:

Variables: H H' S V E2 E1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : sexp (H n1) (sb S (E1 n1)) *
H5 : sexp (H n1) (sb S (E2 n1)) *
============================
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply IH to H1 H4 H3.
Subgoal 6:

Variables: H H' S V E2 E1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : sexp (H n1) (sb S (E1 n1)) *
H5 : sexp (H n1) (sb S (E2 n1)) *
H6 : sexp H' (sb (rep n1 V :: S) (E1 n1))
============================
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply IH to H1 H5 H3.
Subgoal 6:

Variables: H H' S V E2 E1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : sexp (H n1) (sb S (E1 n1)) *
H5 : sexp (H n1) (sb S (E2 n1)) *
H6 : sexp H' (sb (rep n1 V :: S) (E1 n1))
H7 : sexp H' (sb (rep n1 V :: S) (E2 n1))
============================
 sexp H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))

Subgoal 7 is:
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < search.
Subgoal 7:

Variables: H H' S V E2 T1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : {typ T1}
H5 : sexp (val n2 :: H n1) (sb S (E2 n1 n2)) *
============================
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply IH to _ H5 H3.
Subgoal 7:

Variables: H H' S V E2 T1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : {typ T1}
H5 : sexp (val n2 :: H n1) (sb S (E2 n1 n2)) *
H6 : sexp (val n2 :: H') (sb (rep n1 V :: S) (E2 n1 n2))
============================
 sexp H' (sb (rep n1 V :: S) (lam T1 (E2 n1)))

Subgoal 8 is:
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < search.
Subgoal 8:

Variables: H H' S V E2 E1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : sexp (H n1) (sb S (E1 n1)) *
H5 : sexp (H n1) (sb S (E2 n1)) *
============================
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply IH to H1 H4 H3.
Subgoal 8:

Variables: H H' S V E2 E1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : sexp (H n1) (sb S (E1 n1)) *
H5 : sexp (H n1) (sb S (E2 n1)) *
H6 : sexp H' (sb (rep n1 V :: S) (E1 n1))
============================
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < apply IH to H1 H5 H3.
Subgoal 8:

Variables: H H' S V E2 E1
IH : forall H H' S E V, nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) * -> xval V ->
       sexp H' (sb (rep x V :: S) (E x))
H1 : insert (val n1) H' (H n1)
H3 : xval V
H4 : sexp (H n1) (sb S (E1 n1)) *
H5 : sexp (H n1) (sb S (E2 n1)) *
H6 : sexp H' (sb (rep n1 V :: S) (E1 n1))
H7 : sexp H' (sb (rep n1 V :: S) (E2 n1))
============================
 sexp H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1)))

sexp_abs < search.
Proof completed.
Abella < Theorem sub_xval : 
forall S X V, sub S -> member (rep X V) S -> xval V.


============================
 forall S X V, sub S -> member (rep X V) S -> xval V

sub_xval < induction on 1.

IH : forall S X V, sub S * -> member (rep X V) S -> xval V
============================
 forall S X V, sub S @ -> member (rep X V) S -> xval V

sub_xval < intros.

Variables: S X V
IH : forall S X V, sub S * -> member (rep X V) S -> xval V
H1 : sub S @
H2 : member (rep X V) S
============================
 xval V

sub_xval < case H1.
Subgoal 1:

Variables: X V
IH : forall S X V, sub S * -> member (rep X V) S -> xval V
H2 : member (rep X V) nil
============================
 xval V

Subgoal 2 is:
 xval (V n1)

sub_xval < case H2.
Subgoal 2:

Variables: X V S1 V1
IH : forall S X V, sub S * -> member (rep X V) S -> xval V
H2 : member (rep (X n1) (V n1)) (rep n1 V1 :: S1)
H3 : xval V1 *
H4 : sub S1 *
============================
 xval (V n1)

sub_xval < case H2.
Subgoal 2.1:

Variables: S1 V1
IH : forall S X V, sub S * -> member (rep X V) S -> xval V
H3 : xval V1 *
H4 : sub S1 *
============================
 xval V1

Subgoal 2.2 is:
 xval (V n1)

sub_xval < search.
Subgoal 2.2:

Variables: X V S1 V1
IH : forall S X V, sub S * -> member (rep X V) S -> xval V
H3 : xval V1 *
H4 : sub S1 *
H5 : member (rep (X n1) (V n1)) S1
============================
 xval (V n1)

sub_xval < apply IH to H4 H5.
Subgoal 2.2:

Variables: X V S1 V1
IH : forall S X V, sub S * -> member (rep X V) S -> xval V
H3 : xval V1 *
H4 : sub S1 *
H5 : member (rep (X n1) (V n1)) S1
H6 : xval (V n1)
============================
 xval (V n1)

sub_xval < search.
Proof completed.
Abella < Theorem sub_uniq : 
forall S V1 V2, nabla x, sub (S x) -> member (rep x V1) (S x) ->
  member (rep x V2) (S x) -> V1 =
V2.


============================
 forall S V1 V2, nabla x, sub (S x) -> member (rep x V1) (S x) ->
   member (rep x V2) (S x) -> V1 =
 V2

sub_uniq < induction on 1.

IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
============================
 forall S V1 V2, nabla x, sub (S x) @ -> member (rep x V1) (S x) ->
   member (rep x V2) (S x) -> V1 =
 V2

sub_uniq < intros.

Variables: S V1 V2
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H1 : sub (S n1) @
H2 : member (rep n1 V1) (S n1)
H3 : member (rep n1 V2) (S n1)
============================
 V1 = V2

sub_uniq < case H1.
Subgoal 1:

Variables: V1 V2
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H2 : member (rep n1 V1) nil
H3 : member (rep n1 V2) nil
============================
 V1 = V2

Subgoal 2 is:
 V1 n2 = V2 n2

Subgoal 3 is:
 V1 = V2

sub_uniq < case H2.
Subgoal 2:

Variables: V1 V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H2 : member (rep n1 (V1 n2)) (rep n2 (V n1) :: S1 n1)
H3 : member (rep n1 (V2 n2)) (rep n2 (V n1) :: S1 n1)
H4 : xval (V n1) *
H5 : sub (S1 n1) *
============================
 V1 n2 = V2 n2

Subgoal 3 is:
 V1 = V2

sub_uniq < case H2.
Subgoal 2:

Variables: V1 V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H3 : member (rep n1 (V2 n2)) (rep n2 (V n1) :: S1 n1)
H4 : xval (V n1) *
H5 : sub (S1 n1) *
H6 : member (rep n1 (V1 n2)) (S1 n1)
============================
 V1 n2 = V2 n2

Subgoal 3 is:
 V1 = V2

sub_uniq < case H3.
Subgoal 2:

Variables: V1 V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H4 : xval (V n1) *
H5 : sub (S1 n1) *
H6 : member (rep n1 (V1 n2)) (S1 n1)
H7 : member (rep n1 (V2 n2)) (S1 n1)
============================
 V1 n2 = V2 n2

Subgoal 3 is:
 V1 = V2

sub_uniq < apply IH to H5 H6 H7.
Subgoal 2:

Variables: V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H4 : xval (V n1) *
H5 : sub (S1 n1) *
H6 : member (rep n1 (V2 n2)) (S1 n1)
H7 : member (rep n1 (V2 n2)) (S1 n1)
============================
 V2 n2 = V2 n2

Subgoal 3 is:
 V1 = V2

sub_uniq < search.
Subgoal 3:

Variables: V1 V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H2 : member (rep n1 V1) (rep n1 V :: S1)
H3 : member (rep n1 V2) (rep n1 V :: S1)
H4 : xval V *
H5 : sub S1 *
============================
 V1 = V2

sub_uniq < case H2.
Subgoal 3.1:

Variables: V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H3 : member (rep n1 V2) (rep n1 V :: S1)
H4 : xval V *
H5 : sub S1 *
============================
 V = V2

Subgoal 3.2 is:
 V1 = V2

sub_uniq < case H3.
Subgoal 3.1.1:

Variables: S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H4 : xval V *
H5 : sub S1 *
============================
 V = V

Subgoal 3.1.2 is:
 V = V2

Subgoal 3.2 is:
 V1 = V2

sub_uniq < search.
Subgoal 3.1.2:

Variables: V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H4 : xval V *
H5 : sub S1 *
H6 : member (rep n1 V2) S1
============================
 V = V2

Subgoal 3.2 is:
 V1 = V2

sub_uniq < apply member_prune to H6.
Subgoal 3.2:

Variables: V1 V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H3 : member (rep n1 V2) (rep n1 V :: S1)
H4 : xval V *
H5 : sub S1 *
H6 : member (rep n1 V1) S1
============================
 V1 = V2

sub_uniq < case H3.
Subgoal 3.2.1:

Variables: V1 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H4 : xval V *
H5 : sub S1 *
H6 : member (rep n1 V1) S1
============================
 V1 = V

Subgoal 3.2.2 is:
 V1 = V2

sub_uniq < apply member_prune to H6.
Subgoal 3.2.2:

Variables: V1 V2 S1 V
IH : forall S V1 V2, nabla x, sub (S x) * -> member (rep x V1) (S x) ->
       member (rep x V2) (S x) -> V1 =
     V2
H4 : xval V *
H5 : sub S1 *
H6 : member (rep n1 V1) S1
H7 : member (rep n1 V2) S1
============================
 V1 = V2

sub_uniq < apply member_prune to H6.
Proof completed.
Abella < Define ees : sexp -> sexp -> prop by 
nabla x, ees (sb (S x) x) V := nabla x, member (rep x V) (S x);
ees (sb S (num N)) (sb nil (num N)) := {natural N};
ees (sb S (plus E1 E2)) (sb nil (num N)) := exists N1 N2, ees (sb S E1) (sb nil (num N1)) /\
  ees (sb S E2) (sb nil (num N2)) /\ {sum N1 N2 N};
ees (sb S (lam T1 E2)) (sb S (lam T1 E2));
nabla x, ees (sb S (app E1 E2)) (V x) := exists S' T E V2, ees (sb S E1) (sb S' (lam T E)) /\ ees (sb S E2) V2 /\
  (nabla x, ees (sb (rep x V2 :: S') (E x)) (V x)).

Abella < Theorem ees_type : 
forall E V, sexp nil E -> ees E V -> xval V.


============================
 forall E V, sexp nil E -> ees E V -> xval V

ees_type < induction on 2.

IH : forall E V, sexp nil E -> ees E V * -> xval V
============================
 forall E V, sexp nil E -> ees E V @ -> xval V

ees_type < intros.

Variables: E V
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil E
H2 : ees E V @
============================
 xval V

ees_type < case H2.
Subgoal 1:

Variables: V1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb (S n1) n1)
H3 : member (rep n1 V1) (S n1)
============================
 xval V1

Subgoal 2 is:
 xval (sb nil (num N))

Subgoal 3 is:
 xval (sb nil (num N))

Subgoal 4 is:
 xval (sb S (lam T1 E2))

Subgoal 5 is:
 xval (V n1)

ees_type < apply sexp_type to H1.
Subgoal 1:

Variables: V1 S1
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb (S1 n1) n1)
H3 : member (rep n1 V1) (S1 n1)
H4 : vals nil
H5 : sub (S1 n1)
============================
 xval V1

Subgoal 2 is:
 xval (sb nil (num N))

Subgoal 3 is:
 xval (sb nil (num N))

Subgoal 4 is:
 xval (sb S (lam T1 E2))

Subgoal 5 is:
 xval (V n1)

ees_type < apply sub_xval to H5 H3.
Subgoal 1:

Variables: V1 S1
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb (S1 n1) n1)
H3 : member (rep n1 V1) (S1 n1)
H4 : vals nil
H5 : sub (S1 n1)
H6 : xval V1
============================
 xval V1

Subgoal 2 is:
 xval (sb nil (num N))

Subgoal 3 is:
 xval (sb nil (num N))

Subgoal 4 is:
 xval (sb S (lam T1 E2))

Subgoal 5 is:
 xval (V n1)

ees_type < search.
Subgoal 2:

Variables: N S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb S (num N))
H3 : {natural N}
============================
 xval (sb nil (num N))

Subgoal 3 is:
 xval (sb nil (num N))

Subgoal 4 is:
 xval (sb S (lam T1 E2))

Subgoal 5 is:
 xval (V n1)

ees_type < search.
Subgoal 3:

Variables: N1 N2 N E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb S (plus E1 E2))
H3 : ees (sb S E1) (sb nil (num N1)) *
H4 : ees (sb S E2) (sb nil (num N2)) *
H5 : {sum N1 N2 N}
============================
 xval (sb nil (num N))

Subgoal 4 is:
 xval (sb S (lam T1 E2))

Subgoal 5 is:
 xval (V n1)

ees_type < apply sum_type to H5.
Subgoal 3:

Variables: N1 N2 N E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb S (plus E1 E2))
H3 : ees (sb S E1) (sb nil (num N1)) *
H4 : ees (sb S E2) (sb nil (num N2)) *
H5 : {sum N1 N2 N}
H6 : {natural N1}
H7 : {natural N2}
H8 : {natural N}
============================
 xval (sb nil (num N))

Subgoal 4 is:
 xval (sb S (lam T1 E2))

Subgoal 5 is:
 xval (V n1)

ees_type < search.
Subgoal 4:

Variables: E2 T1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb S (lam T1 E2))
============================
 xval (sb S (lam T1 E2))

Subgoal 5 is:
 xval (V n1)

ees_type < search.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H1 : sexp nil (sb S (app E1 E2))
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
============================
 xval (V n1)

ees_type < case H1.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H6 : sexp nil (sb S E1)
H7 : sexp nil (sb S E2)
============================
 xval (V n1)

ees_type < apply IH to H6 H3.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H6 : sexp nil (sb S E1)
H7 : sexp nil (sb S E2)
H8 : xval (sb S' (lam T E3))
============================
 xval (V n1)

ees_type < case H8.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H6 : sexp nil (sb S E1)
H7 : sexp nil (sb S E2)
H9 : sexp nil (sb S' (lam T E3))
============================
 xval (V n1)

ees_type < apply IH to H7 H4.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H6 : sexp nil (sb S E1)
H7 : sexp nil (sb S E2)
H9 : sexp nil (sb S' (lam T E3))
H10 : xval V2
============================
 xval (V n1)

ees_type < case H9.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H6 : sexp nil (sb S E1)
H7 : sexp nil (sb S E2)
H10 : xval V2
H11 : {typ T}
H12 : sexp (val n1 :: nil) (sb S' (E3 n1))
============================
 xval (V n1)

ees_type < apply sexp_abs to _ H12 H10.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H6 : sexp nil (sb S E1)
H7 : sexp nil (sb S E2)
H10 : xval V2
H11 : {typ T}
H12 : sexp (val n1 :: nil) (sb S' (E3 n1))
H13 : sexp nil (sb (rep n1 V2 :: S') (E3 n1))
============================
 xval (V n1)

ees_type < apply IH to H13 H5.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S
IH : forall E V, sexp nil E -> ees E V * -> xval V
H3 : ees (sb S E1) (sb S' (lam T E3)) *
H4 : ees (sb S E2) V2 *
H5 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H6 : sexp nil (sb S E1)
H7 : sexp nil (sb S E2)
H10 : xval V2
H11 : {typ T}
H12 : sexp (val n1 :: nil) (sb S' (E3 n1))
H13 : sexp nil (sb (rep n1 V2 :: S') (E3 n1))
H14 : xval (V n1)
============================
 xval (V n1)

ees_type < search.
Proof completed.
Abella < Define force : olist -> sexp -> exp -> prop by 
nabla x, force (H x) (sb (S x) x) x := nabla x, member (val x) (H x);
nabla x, force (H x) (sb (S x) x) V' := exists V, nabla x, member (rep x V) (S x) /\ force nil V V';
force H (sb S (num N)) (num N);
force H (sb S (plus E1 E2)) (plus E1' E2') := force H (sb S E1) E1' /\ force H (sb S E2) E2';
force H (sb S (lam T1 E2)) (lam T1 E2') := nabla x, force (val x :: H) (sb S (E2 x)) (E2' x);
force H (sb S (app E1 E2)) (app E1' E2') := force H (sb S E1) E1' /\ force H (sb S E2) E2'.

Abella < Theorem force_prune : 
forall H E E', nabla x, force (H x) E (E' x) -> (exists E'', E' = x\E'').


============================
 forall H E E', nabla x, force (H x) E (E' x) -> (exists E'', E' = x\E'')

force_prune < induction on 1.

IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
============================
 forall H E E', nabla x, force (H x) E (E' x) @ -> (exists E'', E' = x\E'')

force_prune < intros.

Variables: H E E'
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H1 : force (H n1) E (E' n1) @
============================
 exists E'', E' = x\E''

force_prune < case H1.
Subgoal 1:

Variables: H E1
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : member (val n2) (H n2 n1)
============================
 exists E'', z2\n2 = x\E''

Subgoal 2 is:
 exists E'', z2\V'1 z2 = x\E''

Subgoal 3 is:
 exists E'', z1\num N = x\E''

Subgoal 4 is:
 exists E'', z1\plus (E1' z1) (E2' z1) = x\E''

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < search.
Subgoal 2:

Variables: H V V'1 E1
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : member (rep n2 (V n1)) (E1 n2)
H3 : force nil (V n1) (V'1 n1) *
============================
 exists E'', z2\V'1 z2 = x\E''

Subgoal 3 is:
 exists E'', z1\num N = x\E''

Subgoal 4 is:
 exists E'', z1\plus (E1' z1) (E2' z1) = x\E''

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < apply member_prune to H2.
Subgoal 2:

Variables: H V'1 E1 E'2
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : member (rep n2 E'2) (E1 n2)
H3 : force nil E'2 (V'1 n1) *
============================
 exists E'', z2\V'1 z2 = x\E''

Subgoal 3 is:
 exists E'', z1\num N = x\E''

Subgoal 4 is:
 exists E'', z1\plus (E1' z1) (E2' z1) = x\E''

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < apply IH to H3.
Subgoal 2:

Variables: H E1 E'2 E''
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : member (rep n2 E'2) (E1 n2)
H3 : force nil E'2 E'' *
============================
 exists E''1, z2\E'' = x\E''1

Subgoal 3 is:
 exists E'', z1\num N = x\E''

Subgoal 4 is:
 exists E'', z1\plus (E1' z1) (E2' z1) = x\E''

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < search.
Subgoal 3:

Variables: H N E1
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
============================
 exists E'', z1\num N = x\E''

Subgoal 4 is:
 exists E'', z1\plus (E1' z1) (E2' z1) = x\E''

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < search.
Subgoal 4:

Variables: H E2' E1' E5 E4 E3
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (H n1) (sb E3 E4) (E1' n1) *
H3 : force (H n1) (sb E3 E5) (E2' n1) *
============================
 exists E'', z1\plus (E1' z1) (E2' z1) = x\E''

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < apply IH to H2.
Subgoal 4:

Variables: H E2' E5 E4 E3 E''
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (H n1) (sb E3 E4) E'' *
H3 : force (H n1) (sb E3 E5) (E2' n1) *
============================
 exists E''1, z1\plus E'' (E2' z1) = x\E''1

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < apply IH to H3.
Subgoal 4:

Variables: H E5 E4 E3 E'' E''1
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (H n1) (sb E3 E4) E'' *
H3 : force (H n1) (sb E3 E5) E''1 *
============================
 exists E''2, z1\plus E'' E''1 = x\E''2

Subgoal 5 is:
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < search.
Subgoal 5:

Variables: H E2' T1 E3 E1
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (val n2 :: H n1) (sb E1 (E3 n2)) (E2' n1 n2) *
============================
 exists E'', z1\lam T1 (E2' z1) = x\E''

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < apply IH to H2.
Subgoal 5:

Variables: H T1 E3 E1 E''
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (val n2 :: H n1) (sb E1 (E3 n2)) (E'' n2) *
============================
 exists E''1, z1\lam T1 (z2\E'' z2) = x\E''1

Subgoal 6 is:
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < search.
Subgoal 6:

Variables: H E2' E1' E5 E4 E3
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (H n1) (sb E3 E4) (E1' n1) *
H3 : force (H n1) (sb E3 E5) (E2' n1) *
============================
 exists E'', z1\app (E1' z1) (E2' z1) = x\E''

force_prune < apply IH to H2.
Subgoal 6:

Variables: H E2' E5 E4 E3 E''
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (H n1) (sb E3 E4) E'' *
H3 : force (H n1) (sb E3 E5) (E2' n1) *
============================
 exists E''1, z1\app E'' (E2' z1) = x\E''1

force_prune < apply IH to H3.
Subgoal 6:

Variables: H E5 E4 E3 E'' E''1
IH : forall H E E', nabla x, force (H x) E (E' x) * ->
       (exists E'', E' = x\E'')
H2 : force (H n1) (sb E3 E4) E'' *
H3 : force (H n1) (sb E3 E5) E''1 *
============================
 exists E''2, z1\app E'' E''1 = x\E''2

force_prune < search.
Proof completed.
Abella < Theorem force_abs : 
forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
  sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) -> xval V ->
  force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V').


============================
 forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
   sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) -> xval V ->
   force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')

force_abs < induction on 3.

IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
============================
 forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
   sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) @ -> xval V ->
   force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')

force_abs < intros.

Variables: H H' S E E' V V'
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S (E n1))
H3 : force (H n1) (sb S (E n1)) (E' n1) @
H4 : xval V
H5 : force nil V V'
============================
 force H' (sb (rep n1 V :: S) (E n1)) (E' V')

force_abs < case H3.
Subgoal 1:

Variables: H H' S V V'
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) (H' n2) (H n2 n1)
H2 : sexp (H n2 n1) (sb (S n2) n2)
H4 : xval (V n2)
H5 : force nil (V n2) (V' n2)
H6 : member (val n2) (H n2 n1)
============================
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) n2

Subgoal 2 is:
 force H' (sb (rep n1 V :: S) n1) V'

Subgoal 3 is:
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) (V'2 (V' n2))

Subgoal 4 is:
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply member_insert to H1 H6.
Subgoal 1:

Variables: H H' S V V'
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) (H' n2) (H n2 n1)
H2 : sexp (H n2 n1) (sb (S n2) n2)
H4 : xval (V n2)
H5 : force nil (V n2) (V' n2)
H6 : member (val n2) (H n2 n1)
H7 : val n1 = val n2 \/ member (val n2) (H' n2)
============================
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) n2

Subgoal 2 is:
 force H' (sb (rep n1 V :: S) n1) V'

Subgoal 3 is:
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) (V'2 (V' n2))

Subgoal 4 is:
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < case H7.
Subgoal 1:

Variables: H H' S V V'
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) (H' n2) (H n2 n1)
H2 : sexp (H n2 n1) (sb (S n2) n2)
H4 : xval (V n2)
H5 : force nil (V n2) (V' n2)
H6 : member (val n2) (H n2 n1)
H8 : member (val n2) (H' n2)
============================
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) n2

Subgoal 2 is:
 force H' (sb (rep n1 V :: S) n1) V'

Subgoal 3 is:
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) (V'2 (V' n2))

Subgoal 4 is:
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Subgoal 2:

Variables: H H' S V V'
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S n1)
H4 : xval V
H5 : force nil V V'
H6 : member (val n1) (H n1)
============================
 force H' (sb (rep n1 V :: S) n1) V'

Subgoal 3 is:
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) (V'2 (V' n2))

Subgoal 4 is:
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Subgoal 3:

Variables: H H' S V V' V1 V'2
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) (H' n2) (H n2 n1)
H2 : sexp (H n2 n1) (sb (S n2) n2)
H4 : xval (V n2)
H5 : force nil (V n2) (V' n2)
H6 : member (rep n2 (V1 n1)) (S n2)
H7 : force nil (V1 n1) (V'2 n1) *
============================
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) (V'2 (V' n2))

Subgoal 4 is:
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply member_prune to H6.
Subgoal 3:

Variables: H H' S V V' V'2 E'2
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) (H' n2) (H n2 n1)
H2 : sexp (H n2 n1) (sb (S n2) n2)
H4 : xval (V n2)
H5 : force nil (V n2) (V' n2)
H6 : member (rep n2 E'2) (S n2)
H7 : force nil E'2 (V'2 n1) *
============================
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) (V'2 (V' n2))

Subgoal 4 is:
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply force_prune to H7.
Subgoal 3:

Variables: H H' S V V' E'2 E''
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) (H' n2) (H n2 n1)
H2 : sexp (H n2 n1) (sb (S n2) n2)
H4 : xval (V n2)
H5 : force nil (V n2) (V' n2)
H6 : member (rep n2 E'2) (S n2)
H7 : force nil E'2 E'' *
============================
 force (H' n2) (sb (rep n1 (V n2) :: S n2) n2) E''

Subgoal 4 is:
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Subgoal 4:

Variables: H H' S V V' V1 V'1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S n1)
H4 : xval V
H5 : force nil V V'
H6 : member (rep n1 V1) S
H7 : force nil V1 V'1 *
============================
 force H' (sb (rep n1 V :: S) n1) V'1

Subgoal 5 is:
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Subgoal 5:

Variables: H H' S V V' N
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S (num N))
H4 : xval V
H5 : force nil V V'
============================
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < case H2.
Subgoal 5:

Variables: H H' S V V' N
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : vals (H n1)
H7 : sub S
H8 : {natural N}
============================
 force H' (sb (rep n1 V :: S) (num N)) (num N)

Subgoal 6 is:
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Subgoal 6:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S (plus (E1 n1) (E2 n1)))
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
============================
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < case H2.
Subgoal 6:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
H8 : sexp (H n1) (sb S (E1 n1))
H9 : sexp (H n1) (sb S (E2 n1))
============================
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply IH to H1 H8 H6 H4 H5.
Subgoal 6:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
H8 : sexp (H n1) (sb S (E1 n1))
H9 : sexp (H n1) (sb S (E2 n1))
H10 : force H' (sb (rep n1 V :: S) (E1 n1)) (E1' V')
============================
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply IH to H1 H9 H7 H4 H5.
Subgoal 6:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
H8 : sexp (H n1) (sb S (E1 n1))
H9 : sexp (H n1) (sb S (E2 n1))
H10 : force H' (sb (rep n1 V :: S) (E1 n1)) (E1' V')
H11 : force H' (sb (rep n1 V :: S) (E2 n1)) (E2' V')
============================
 force H' (sb (rep n1 V :: S) (plus (E1 n1) (E2 n1)))
   (plus (E1' V') (E2' V'))

Subgoal 7 is:
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Subgoal 7:

Variables: H H' S V V' E2' T1 E2
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S (lam T1 (E2 n1)))
H4 : xval V
H5 : force nil V V'
H6 : force (val n2 :: H n1) (sb S (E2 n1 n2)) (E2' n1 n2) *
============================
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < case H2.
Subgoal 7:

Variables: H H' S V V' E2' T1 E2
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (val n2 :: H n1) (sb S (E2 n1 n2)) (E2' n1 n2) *
H7 : {typ T1}
H8 : sexp (val n2 :: H n1) (sb S (E2 n1 n2))
============================
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply IH to _ H8 H6 H4 H5.
Subgoal 7:

Variables: H H' S V V' E2' T1 E2
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (val n2 :: H n1) (sb S (E2 n1 n2)) (E2' n1 n2) *
H7 : {typ T1}
H8 : sexp (val n2 :: H n1) (sb S (E2 n1 n2))
H9 : force (val n2 :: H') (sb (rep n1 V :: S) (E2 n1 n2)) (E2' V' n2)
============================
 force H' (sb (rep n1 V :: S) (lam T1 (E2 n1))) (lam T1 (E2' V'))

Subgoal 8 is:
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Subgoal 8:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H2 : sexp (H n1) (sb S (app (E1 n1) (E2 n1)))
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
============================
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < case H2.
Subgoal 8:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
H8 : sexp (H n1) (sb S (E1 n1))
H9 : sexp (H n1) (sb S (E2 n1))
============================
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply IH to H1 H8 H6 H4 H5.
Subgoal 8:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
H8 : sexp (H n1) (sb S (E1 n1))
H9 : sexp (H n1) (sb S (E2 n1))
H10 : force H' (sb (rep n1 V :: S) (E1 n1)) (E1' V')
============================
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < apply IH to H1 H9 H7 H4 H5.
Subgoal 8:

Variables: H H' S V V' E2' E1' E2 E1
IH : forall H H' S E E' V V', nabla x, insert (val x) H' (H x) ->
       sexp (H x) (sb S (E x)) -> force (H x) (sb S (E x)) (E' x) * ->
       xval V -> force nil V V' -> force H' (sb (rep x V :: S) (E x)) (E' V')
H1 : insert (val n1) H' (H n1)
H4 : xval V
H5 : force nil V V'
H6 : force (H n1) (sb S (E1 n1)) (E1' n1) *
H7 : force (H n1) (sb S (E2 n1)) (E2' n1) *
H8 : sexp (H n1) (sb S (E1 n1))
H9 : sexp (H n1) (sb S (E2 n1))
H10 : force H' (sb (rep n1 V :: S) (E1 n1)) (E1' V')
H11 : force H' (sb (rep n1 V :: S) (E2 n1)) (E2' V')
============================
 force H' (sb (rep n1 V :: S) (app (E1 n1) (E2 n1))) (app (E1' V') (E2' V'))

force_abs < search.
Proof completed.
Abella < Theorem force_inv : 
forall V V', force nil V V' -> xval V ->
  (exists N, V = sb nil (num N) /\ V' = num N /\ {natural N}) \/
  (exists S T E E', V = sb S (lam T E) /\ V' = lam T E').


============================
 forall V V', force nil V V' -> xval V ->
   (exists N, V = sb nil (num N) /\ V' = num N /\ {natural N}) \/
   (exists S T E E', V = sb S (lam T E) /\ V' = lam T E')

force_inv < intros.

Variables: V V'
H1 : force nil V V'
H2 : xval V
============================
 (exists N, V = sb nil (num N) /\ V' = num N /\ {natural N}) \/
   (exists S T E E', V = sb S (lam T E) /\ V' = lam T E')

force_inv < case H2.
Subgoal 1:

Variables: V' N
H1 : force nil (sb nil (num N)) V'
H3 : {natural N}
============================
 (exists N1, sb nil (num N) = sb nil (num N1) /\ V' = num N1 /\ {natural N1}) \/
   (exists S T E E', sb nil (num N) = sb S (lam T E) /\ V' = lam T E')

Subgoal 2 is:
 (exists N, sb S (lam T1 E2) = sb nil (num N) /\ V' = num N /\ {natural N}) \/
   (exists S1 T E E', sb S (lam T1 E2) = sb S1 (lam T E) /\ V' = lam T E')

force_inv < case H1.
Subgoal 1:

Variables: N
H3 : {natural N}
============================
 (exists N1, sb nil (num N) = sb nil (num N1) /\ num N = num N1 /\
      {natural N1}) \/
   (exists S T E E', sb nil (num N) = sb S (lam T E) /\ num N = lam T E')

Subgoal 2 is:
 (exists N, sb S (lam T1 E2) = sb nil (num N) /\ V' = num N /\ {natural N}) \/
   (exists S1 T E E', sb S (lam T1 E2) = sb S1 (lam T E) /\ V' = lam T E')

force_inv < search.
Subgoal 2:

Variables: V' E2 T1 S
H1 : force nil (sb S (lam T1 E2)) V'
H3 : sexp nil (sb S (lam T1 E2))
============================
 (exists N, sb S (lam T1 E2) = sb nil (num N) /\ V' = num N /\ {natural N}) \/
   (exists S1 T E E', sb S (lam T1 E2) = sb S1 (lam T E) /\ V' = lam T E')

force_inv < case H1.
Subgoal 2:

Variables: E2 T1 S E2'
H3 : sexp nil (sb S (lam T1 E2))
H4 : force (val n1 :: nil) (sb S (E2 n1)) (E2' n1)
============================
 (exists N, sb S (lam T1 E2) = sb nil (num N) /\ lam T1 E2' = num N /\
      {natural N}) \/
   (exists S1 T E E', sb S (lam T1 E2) = sb S1 (lam T E) /\ lam T1 E2' =
      lam T E')

force_inv < search.
Proof completed.
Abella < Theorem ees_eval : 
forall E V E', sexp nil E -> force nil E E' -> ees E V ->
  (exists V', force nil V V' /\ {eval E' V'}).


============================
 forall E V E', sexp nil E -> force nil E E' -> ees E V ->
   (exists V', force nil V V' /\ {eval E' V'})

ees_eval < induction on 3.

IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
============================
 forall E V E', sexp nil E -> force nil E E' -> ees E V @ ->
   (exists V', force nil V V' /\ {eval E' V'})

ees_eval < intros.

Variables: E V E'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil E
H2 : force nil E E'
H3 : ees E V @
============================
 exists V', force nil V V' /\ {eval E' V'}

ees_eval < case H3.
Subgoal 1:

Variables: E' V1 S
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S n1) n1)
H2 : force nil (sb (S n1) n1) (E' n1)
H4 : member (rep n1 V1) (S n1)
============================
 exists V', force nil V1 V' /\ {eval (E' n1) V'}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H2.
Subgoal 1.1:

Variables: V1 S
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S n1) n1)
H4 : member (rep n1 V1) (S n1)
H5 : member (val n1) nil
============================
 exists V', force nil V1 V' /\ {eval n1 V'}

Subgoal 1.2 is:
 exists V'1, force nil V1 V'1 /\ {eval V' V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H5.
Subgoal 1.2:

Variables: V1 S V2 V'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S n1) n1)
H4 : member (rep n1 V1) (S n1)
H5 : member (rep n1 V2) (S n1)
H6 : force nil V2 V'
============================
 exists V'1, force nil V1 V'1 /\ {eval V' V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < apply sexp_type to H1.
Subgoal 1.2:

Variables: V1 V2 V' S1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S1 n1) n1)
H4 : member (rep n1 V1) (S1 n1)
H5 : member (rep n1 V2) (S1 n1)
H6 : force nil V2 V'
H7 : vals nil
H8 : sub (S1 n1)
============================
 exists V'1, force nil V1 V'1 /\ {eval V' V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < apply sub_uniq to H8 H4 H5.
Subgoal 1.2:

Variables: V2 V' S1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S1 n1) n1)
H4 : member (rep n1 V2) (S1 n1)
H5 : member (rep n1 V2) (S1 n1)
H6 : force nil V2 V'
H7 : vals nil
H8 : sub (S1 n1)
============================
 exists V'1, force nil V2 V'1 /\ {eval V' V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < apply sub_xval to H8 H4.
Subgoal 1.2:

Variables: V2 V' S1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S1 n1) n1)
H4 : member (rep n1 V2) (S1 n1)
H5 : member (rep n1 V2) (S1 n1)
H6 : force nil V2 V'
H7 : vals nil
H8 : sub (S1 n1)
H9 : xval V2
============================
 exists V'1, force nil V2 V'1 /\ {eval V' V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < apply force_inv to H6 H9.
Subgoal 1.2:

Variables: V2 V' S1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S1 n1) n1)
H4 : member (rep n1 V2) (S1 n1)
H5 : member (rep n1 V2) (S1 n1)
H6 : force nil V2 V'
H7 : vals nil
H8 : sub (S1 n1)
H9 : xval V2
H10 : (exists N, V2 = sb nil (num N) /\ V' = num N /\ {natural N}) \/
        (exists S T E E', V2 = sb S (lam T E) /\ V' = lam T E')
============================
 exists V'1, force nil V2 V'1 /\ {eval V' V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H10.
Subgoal 1.2.1:

Variables: S1 N
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S1 n1) n1)
H4 : member (rep n1 (sb nil (num N))) (S1 n1)
H5 : member (rep n1 (sb nil (num N))) (S1 n1)
H6 : force nil (sb nil (num N)) (num N)
H7 : vals nil
H8 : sub (S1 n1)
H9 : xval (sb nil (num N))
H11 : {natural N}
============================
 exists V'1, force nil (sb nil (num N)) V'1 /\ {eval (num N) V'1}

Subgoal 1.2.2 is:
 exists V'1, force nil (sb S2 (lam T E2)) V'1 /\ {eval (lam T E'1) V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < search.
Subgoal 1.2.2:

Variables: S1 S2 T E2 E'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb (S1 n1) n1)
H4 : member (rep n1 (sb S2 (lam T E2))) (S1 n1)
H5 : member (rep n1 (sb S2 (lam T E2))) (S1 n1)
H6 : force nil (sb S2 (lam T E2)) (lam T E'1)
H7 : vals nil
H8 : sub (S1 n1)
H9 : xval (sb S2 (lam T E2))
============================
 exists V'1, force nil (sb S2 (lam T E2)) V'1 /\ {eval (lam T E'1) V'1}

Subgoal 2 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < search.
Subgoal 2:

Variables: E' N S
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (num N))
H2 : force nil (sb S (num N)) E'
H4 : {natural N}
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H2.
Subgoal 2:

Variables: N S
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (num N))
H4 : {natural N}
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval (num N) V'}

Subgoal 3 is:
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < search.
Subgoal 3:

Variables: E' N1 N2 N E2 E1 S
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (plus E1 E2))
H2 : force nil (sb S (plus E1 E2)) E'
H4 : ees (sb S E1) (sb nil (num N1)) *
H5 : ees (sb S E2) (sb nil (num N2)) *
H6 : {sum N1 N2 N}
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval E' V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H2.
Subgoal 3:

Variables: N1 N2 N E2 E1 S E2' E1'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (plus E1 E2))
H4 : ees (sb S E1) (sb nil (num N1)) *
H5 : ees (sb S E2) (sb nil (num N2)) *
H6 : {sum N1 N2 N}
H7 : force nil (sb S E1) E1'
H8 : force nil (sb S E2) E2'
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval (plus E1' E2') V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H1.
Subgoal 3:

Variables: N1 N2 N E2 E1 S E2' E1'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb nil (num N1)) *
H5 : ees (sb S E2) (sb nil (num N2)) *
H6 : {sum N1 N2 N}
H7 : force nil (sb S E1) E1'
H8 : force nil (sb S E2) E2'
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval (plus E1' E2') V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < apply IH to H9 H7 H4.
Subgoal 3:

Variables: N1 N2 N E2 E1 S E2' E1' V'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb nil (num N1)) *
H5 : ees (sb S E2) (sb nil (num N2)) *
H6 : {sum N1 N2 N}
H7 : force nil (sb S E1) E1'
H8 : force nil (sb S E2) E2'
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H11 : force nil (sb nil (num N1)) V'
H12 : {eval E1' V'}
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval (plus E1' E2') V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H11.
Subgoal 3:

Variables: N1 N2 N E2 E1 S E2' E1'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb nil (num N1)) *
H5 : ees (sb S E2) (sb nil (num N2)) *
H6 : {sum N1 N2 N}
H7 : force nil (sb S E1) E1'
H8 : force nil (sb S E2) E2'
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E1' (num N1)}
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval (plus E1' E2') V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < apply IH to H10 H8 H5.
Subgoal 3:

Variables: N1 N2 N E2 E1 S E2' E1' V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb nil (num N1)) *
H5 : ees (sb S E2) (sb nil (num N2)) *
H6 : {sum N1 N2 N}
H7 : force nil (sb S E1) E1'
H8 : force nil (sb S E2) E2'
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E1' (num N1)}
H13 : force nil (sb nil (num N2)) V'1
H14 : {eval E2' V'1}
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval (plus E1' E2') V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H13.
Subgoal 3:

Variables: N1 N2 N E2 E1 S E2' E1'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb nil (num N1)) *
H5 : ees (sb S E2) (sb nil (num N2)) *
H6 : {sum N1 N2 N}
H7 : force nil (sb S E1) E1'
H8 : force nil (sb S E2) E2'
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E1' (num N1)}
H14 : {eval E2' (num N2)}
============================
 exists V', force nil (sb nil (num N)) V' /\ {eval (plus E1' E2') V'}

Subgoal 4 is:
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < search.
Subgoal 4:

Variables: E' E2 T1 S
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (lam T1 E2))
H2 : force nil (sb S (lam T1 E2)) E'
============================
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval E' V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H2.
Subgoal 4:

Variables: E2 T1 S E2'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (lam T1 E2))
H4 : force (val n1 :: nil) (sb S (E2 n1)) (E2' n1)
============================
 exists V', force nil (sb S (lam T1 E2)) V' /\ {eval (lam T1 E2') V'}

Subgoal 5 is:
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < search.
Subgoal 5:

Variables: V E' S' T E3 V2 E2 E1 S
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (app E1 E2))
H2 : force nil (sb S (app E1 E2)) (E' n1)
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
============================
 exists V', force nil (V n1) V' /\ {eval (E' n1) V'}

ees_eval < case H2.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E2' E1'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H1 : sexp nil (sb S (app E1 E2))
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) (E1' n1)
H8 : force nil (sb S E2) (E2' n1)
============================
 exists V', force nil (V n1) V' /\ {eval (app (E1' n1) (E2' n1)) V'}

ees_eval < case H1.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E2' E1'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) (E1' n1)
H8 : force nil (sb S E2) (E2' n1)
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
============================
 exists V', force nil (V n1) V' /\ {eval (app (E1' n1) (E2' n1)) V'}

ees_eval < apply force_prune to H7.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E2' E''
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) (E2' n1)
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' (E2' n1)) V'}

ees_eval < apply force_prune to H8.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < apply IH to H9 H7 H4.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 V'
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H11 : force nil (sb S' (lam T E3)) V'
H12 : {eval E'' V'}
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < case H11.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < apply IH to H10 H8 H5.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < apply ees_type to H9 H4.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
H16 : xval (sb S' (lam T E3))
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < case H16.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
H17 : sexp nil (sb S' (lam T E3))
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < case H17.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
H18 : {typ T}
H19 : sexp (val n1 :: nil) (sb S' (E3 n1))
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < apply ees_type to H10 H5.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
H18 : {typ T}
H19 : sexp (val n1 :: nil) (sb S' (E3 n1))
H20 : xval V2
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < apply sexp_abs to _ H19 H20.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
H18 : {typ T}
H19 : sexp (val n1 :: nil) (sb S' (E3 n1))
H20 : xval V2
H21 : sexp nil (sb (rep n1 V2 :: S') (E3 n1))
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < apply force_abs to _ H19 H13 H20 H14.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
H18 : {typ T}
H19 : sexp (val n1 :: nil) (sb S' (E3 n1))
H20 : xval V2
H21 : sexp nil (sb (rep n1 V2 :: S') (E3 n1))
H22 : force nil (sb (rep n1 V2 :: S') (E3 n1)) (E2'1 V'1)
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < apply IH to H21 H22 H6.
Subgoal 5:

Variables: V S' T E3 V2 E2 E1 S E'' E''1 E2'1 V'1 V'2
IH : forall E V E', sexp nil E -> force nil E E' -> ees E V * ->
       (exists V', force nil V V' /\ {eval E' V'})
H4 : ees (sb S E1) (sb S' (lam T E3)) *
H5 : ees (sb S E2) V2 *
H6 : ees (sb (rep n1 V2 :: S') (E3 n1)) (V n1) *
H7 : force nil (sb S E1) E''
H8 : force nil (sb S E2) E''1
H9 : sexp nil (sb S E1)
H10 : sexp nil (sb S E2)
H12 : {eval E'' (lam T E2'1)}
H13 : force (val n1 :: nil) (sb S' (E3 n1)) (E2'1 n1)
H14 : force nil V2 V'1
H15 : {eval E''1 V'1}
H18 : {typ T}
H19 : sexp (val n1 :: nil) (sb S' (E3 n1))
H20 : xval V2
H21 : sexp nil (sb (rep n1 V2 :: S') (E3 n1))
H22 : force nil (sb (rep n1 V2 :: S') (E3 n1)) (E2'1 V'1)
H23 : force nil (V n1) (V'2 n1)
H24 : {eval (E2'1 V'1) (V'2 n1)}
============================
 exists V', force nil (V n1) V' /\ {eval (app E'' E''1) V'}

ees_eval < search.
Proof completed.
Abella < Theorem eval_ees : 
forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'} ->
  (exists V, force nil V V' /\ ees E V).


============================
 forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'} ->
   (exists V, force nil V V' /\ ees E V)

eval_ees < induction on 3.

IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
============================
 forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}@ ->
   (exists V, force nil V V' /\ ees E V)

eval_ees < intros.

Variables: E E' V'
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil E
H2 : force nil E E'
H3 : {eval E' V'}@
============================
 exists V, force nil V V' /\ ees E V

eval_ees < apply sexp_type to H1.

Variables: E' V' S E1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S E1)
H2 : force nil (sb S E1) E'
H3 : {eval E' V'}@
H4 : vals nil
H5 : sub S
============================
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H3.
Subgoal 1:

Variables: S E1 N
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S E1)
H2 : force nil (sb S E1) (num N)
H4 : vals nil
H5 : sub S
H6 : {natural N}*
============================
 exists V, force nil V (num N) /\ ees (sb S E1) V

Subgoal 2 is:
 exists V, force nil V (num N) /\ ees (sb S E1) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H2.
Subgoal 1.1:

Variables: S N V
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : {natural N}*
H7 : member (rep n1 V) (S n1)
H8 : force nil V (num N)
============================
 exists V, force nil V (num N) /\ ees (sb (S n1) n1) V

Subgoal 1.2 is:
 exists V, force nil V (num N) /\ ees (sb S (num N)) V

Subgoal 2 is:
 exists V, force nil V (num N) /\ ees (sb S E1) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < search.
Subgoal 1.2:

Variables: S N
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S (num N))
H4 : vals nil
H5 : sub S
H6 : {natural N}*
============================
 exists V, force nil V (num N) /\ ees (sb S (num N)) V

Subgoal 2 is:
 exists V, force nil V (num N) /\ ees (sb S E1) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < search.
Subgoal 2:

Variables: S E1 N N2 N1 E2 E3
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S E1)
H2 : force nil (sb S E1) (plus E3 E2)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N1)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N1 N2 N}*
============================
 exists V, force nil V (num N) /\ ees (sb S E1) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H2.
Subgoal 2.1:

Variables: S N N2 N1 V V'3 V'2
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : {eval V'2 (num N1)}*
H7 : {eval V'3 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : member (rep n1 V) (S n1)
H10 : force nil V (plus V'2 V'3)
============================
 exists V, force nil V (num N) /\ ees (sb (S n1) n1) V

Subgoal 2.2 is:
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply sub_xval to H5 H9.
Subgoal 2.1:

Variables: S N N2 N1 V V'3 V'2
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : {eval V'2 (num N1)}*
H7 : {eval V'3 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : member (rep n1 V) (S n1)
H10 : force nil V (plus V'2 V'3)
H11 : xval V
============================
 exists V, force nil V (num N) /\ ees (sb (S n1) n1) V

Subgoal 2.2 is:
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply force_inv to H10 H11.
Subgoal 2.1:

Variables: S N N2 N1 V V'3 V'2
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : {eval V'2 (num N1)}*
H7 : {eval V'3 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : member (rep n1 V) (S n1)
H10 : force nil V (plus V'2 V'3)
H11 : xval V
H12 : (exists N, V = sb nil (num N) /\ plus V'2 V'3 = num N /\ {natural N}) \/
        (exists S T E E', V = sb S (lam T E) /\ plus V'2 V'3 = lam T E')
============================
 exists V, force nil V (num N) /\ ees (sb (S n1) n1) V

Subgoal 2.2 is:
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H12.
Subgoal 2.2:

Variables: S N N2 N1 E2 E3 E5 E4
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S (plus E4 E5))
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N1)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H1.
Subgoal 2.2:

Variables: S N N2 N1 E2 E3 E5 E4
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N1)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply IH to H11 H9 H6.
Subgoal 2.2:

Variables: S N N2 N1 E2 E3 E5 E4 V
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N1)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil V (num N1)
H14 : ees (sb S E4) V
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply ees_type to H11 H14.
Subgoal 2.2:

Variables: S N N2 N1 E2 E3 E5 E4 V
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N1)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil V (num N1)
H14 : ees (sb S E4) V
H15 : xval V
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply force_inv to H13 H15.
Subgoal 2.2:

Variables: S N N2 N1 E2 E3 E5 E4 V
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N1)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N1 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil V (num N1)
H14 : ees (sb S E4) V
H15 : xval V
H16 : (exists N, V = sb nil (num N) /\ num N1 = num N /\ {natural N}) \/
        (exists S T E E', V = sb S (lam T E) /\ num N1 = lam T E')
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H16.
Subgoal 2.2:

Variables: S N N2 E2 E3 E5 E4 N3
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N3)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N3 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil (sb nil (num N3)) (num N3)
H14 : ees (sb S E4) (sb nil (num N3))
H15 : xval (sb nil (num N3))
H17 : {natural N3}
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply IH to H12 H10 H7.
Subgoal 2.2:

Variables: S N N2 E2 E3 E5 E4 N3 V1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N3)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N3 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil (sb nil (num N3)) (num N3)
H14 : ees (sb S E4) (sb nil (num N3))
H15 : xval (sb nil (num N3))
H17 : {natural N3}
H18 : force nil V1 (num N2)
H19 : ees (sb S E5) V1
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply ees_type to H12 H19.
Subgoal 2.2:

Variables: S N N2 E2 E3 E5 E4 N3 V1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N3)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N3 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil (sb nil (num N3)) (num N3)
H14 : ees (sb S E4) (sb nil (num N3))
H15 : xval (sb nil (num N3))
H17 : {natural N3}
H18 : force nil V1 (num N2)
H19 : ees (sb S E5) V1
H20 : xval V1
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < apply force_inv to H18 H20.
Subgoal 2.2:

Variables: S N N2 E2 E3 E5 E4 N3 V1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N3)}*
H7 : {eval E2 (num N2)}*
H8 : {sum N3 N2 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil (sb nil (num N3)) (num N3)
H14 : ees (sb S E4) (sb nil (num N3))
H15 : xval (sb nil (num N3))
H17 : {natural N3}
H18 : force nil V1 (num N2)
H19 : ees (sb S E5) V1
H20 : xval V1
H21 : (exists N, V1 = sb nil (num N) /\ num N2 = num N /\ {natural N}) \/
        (exists S T E E', V1 = sb S (lam T E) /\ num N2 = lam T E')
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H21.
Subgoal 2.2:

Variables: S N E2 E3 E5 E4 N3 N4
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E3 (num N3)}*
H7 : {eval E2 (num N4)}*
H8 : {sum N3 N4 N}*
H9 : force nil (sb S E4) E3
H10 : force nil (sb S E5) E2
H11 : sexp nil (sb S E4)
H12 : sexp nil (sb S E5)
H13 : force nil (sb nil (num N3)) (num N3)
H14 : ees (sb S E4) (sb nil (num N3))
H15 : xval (sb nil (num N3))
H17 : {natural N3}
H18 : force nil (sb nil (num N4)) (num N4)
H19 : ees (sb S E5) (sb nil (num N4))
H20 : xval (sb nil (num N4))
H22 : {natural N4}
============================
 exists V, force nil V (num N) /\ ees (sb S (plus E4 E5)) V

Subgoal 3 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < search.
Subgoal 3:

Variables: S E1 E2 T1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S E1)
H2 : force nil (sb S E1) (lam T1 E2)
H4 : vals nil
H5 : sub S
============================
 exists V, force nil V (lam T1 E2) /\ ees (sb S E1) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H2.
Subgoal 3.1:

Variables: S T1 V V'2
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : member (rep n1 V) (S n1)
H7 : force nil V (lam T1 V'2)
============================
 exists V, force nil V (lam T1 V'2) /\ ees (sb (S n1) n1) V

Subgoal 3.2 is:
 exists V, force nil V (lam T1 E2) /\ ees (sb S (lam T1 E3)) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < search.
Subgoal 3.2:

Variables: S E2 T1 E3
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S (lam T1 E3))
H4 : vals nil
H5 : sub S
H6 : force (val n1 :: nil) (sb S (E3 n1)) (E2 n1)
============================
 exists V, force nil V (lam T1 E2) /\ ees (sb S (lam T1 E3)) V

Subgoal 4 is:
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < search.
Subgoal 4:

Variables: V' S E1 V2 E2 E3 T E4
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S E1)
H2 : force nil (sb S E1) (app E4 E3)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T E2)}*
H7 : {eval E3 V2}*
H8 : {eval (E2 V2) V'}*
============================
 exists V, force nil V V' /\ ees (sb S E1) V

eval_ees < case H2.
Subgoal 4.1:

Variables: V' S V2 E2 T V V'3 V'2
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : {eval V'2 (lam T (E2 n1))}*
H7 : {eval V'3 (V2 n1)}*
H8 : {eval (E2 n1 (V2 n1)) (V' n1)}*
H9 : member (rep n1 V) (S n1)
H10 : force nil V (app V'2 V'3)
============================
 exists V, force nil V (V' n1) /\ ees (sb (S n1) n1) V

Subgoal 4.2 is:
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply sub_xval to H5 H9.
Subgoal 4.1:

Variables: V' S V2 E2 T V V'3 V'2
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : {eval V'2 (lam T (E2 n1))}*
H7 : {eval V'3 (V2 n1)}*
H8 : {eval (E2 n1 (V2 n1)) (V' n1)}*
H9 : member (rep n1 V) (S n1)
H10 : force nil V (app V'2 V'3)
H11 : xval V
============================
 exists V, force nil V (V' n1) /\ ees (sb (S n1) n1) V

Subgoal 4.2 is:
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply force_inv to H10 H11.
Subgoal 4.1:

Variables: V' S V2 E2 T V V'3 V'2
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb (S n1) n1)
H4 : vals nil
H5 : sub (S n1)
H6 : {eval V'2 (lam T (E2 n1))}*
H7 : {eval V'3 (V2 n1)}*
H8 : {eval (E2 n1 (V2 n1)) (V' n1)}*
H9 : member (rep n1 V) (S n1)
H10 : force nil V (app V'2 V'3)
H11 : xval V
H12 : (exists N, V = sb nil (num N) /\ app V'2 V'3 = num N /\ {natural N}) \/
        (exists S T E E', V = sb S (lam T E) /\ app V'2 V'3 = lam T E')
============================
 exists V, force nil V (V' n1) /\ ees (sb (S n1) n1) V

Subgoal 4.2 is:
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < case H12.
Subgoal 4.2:

Variables: V' S V2 E2 E3 T E4 E6 E5
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H1 : sexp nil (sb S (app E5 E6))
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T E2)}*
H7 : {eval E3 V2}*
H8 : {eval (E2 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < case H1.
Subgoal 4.2:

Variables: V' S V2 E2 E3 T E4 E6 E5
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T E2)}*
H7 : {eval E3 V2}*
H8 : {eval (E2 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply IH to H11 H9 H6.
Subgoal 4.2:

Variables: V' S V2 E2 E3 T E4 E6 E5 V
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T E2)}*
H7 : {eval E3 V2}*
H8 : {eval (E2 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H13 : force nil V (lam T E2)
H14 : ees (sb S E5) V
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply ees_type to H11 H14.
Subgoal 4.2:

Variables: V' S V2 E2 E3 T E4 E6 E5 V
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T E2)}*
H7 : {eval E3 V2}*
H8 : {eval (E2 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H13 : force nil V (lam T E2)
H14 : ees (sb S E5) V
H15 : xval V
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply force_inv to H13 H15.
Subgoal 4.2:

Variables: V' S V2 E2 E3 T E4 E6 E5 V
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T E2)}*
H7 : {eval E3 V2}*
H8 : {eval (E2 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H13 : force nil V (lam T E2)
H14 : ees (sb S E5) V
H15 : xval V
H16 : (exists N, V = sb nil (num N) /\ lam T E2 = num N /\ {natural N}) \/
        (exists S T1 E E', V = sb S (lam T1 E) /\ lam T E2 = lam T1 E')
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < case H16.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H13 : force nil (sb S1 (lam T1 E7)) (lam T1 E'1)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H15 : xval (sb S1 (lam T1 E7))
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < case H13.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H15 : xval (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < case H15.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
H18 : sexp nil (sb S1 (lam T1 E7))
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < case H18.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
H19 : {typ T1}
H20 : sexp (val n1 :: nil) (sb S1 (E7 n1))
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply IH to H12 H10 H7.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1 V1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
H19 : {typ T1}
H20 : sexp (val n1 :: nil) (sb S1 (E7 n1))
H21 : force nil V1 V2
H22 : ees (sb S E6) V1
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply ees_type to H12 H22.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1 V1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
H19 : {typ T1}
H20 : sexp (val n1 :: nil) (sb S1 (E7 n1))
H21 : force nil V1 V2
H22 : ees (sb S E6) V1
H23 : xval V1
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply sexp_abs to _ H20 H23.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1 V1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
H19 : {typ T1}
H20 : sexp (val n1 :: nil) (sb S1 (E7 n1))
H21 : force nil V1 V2
H22 : ees (sb S E6) V1
H23 : xval V1
H24 : sexp nil (sb (rep n1 V1 :: S1) (E7 n1))
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply force_abs to _ H20 H17 H23 H21.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1 V1
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
H19 : {typ T1}
H20 : sexp (val n1 :: nil) (sb S1 (E7 n1))
H21 : force nil V1 V2
H22 : ees (sb S E6) V1
H23 : xval V1
H24 : sexp nil (sb (rep n1 V1 :: S1) (E7 n1))
H25 : force nil (sb (rep n1 V1 :: S1) (E7 n1)) (E'1 V2)
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < apply IH to H24 H25 H8.
Subgoal 4.2:

Variables: V' S V2 E3 E4 E6 E5 S1 T1 E7 E'1 V1 V3
IH : forall E E' V', sexp nil E -> force nil E E' -> {eval E' V'}* ->
       (exists V, force nil V V' /\ ees E V)
H4 : vals nil
H5 : sub S
H6 : {eval E4 (lam T1 E'1)}*
H7 : {eval E3 V2}*
H8 : {eval (E'1 V2) V'}*
H9 : force nil (sb S E5) E4
H10 : force nil (sb S E6) E3
H11 : sexp nil (sb S E5)
H12 : sexp nil (sb S E6)
H14 : ees (sb S E5) (sb S1 (lam T1 E7))
H17 : force (val n1 :: nil) (sb S1 (E7 n1)) (E'1 n1)
H19 : {typ T1}
H20 : sexp (val n1 :: nil) (sb S1 (E7 n1))
H21 : force nil V1 V2
H22 : ees (sb S E6) V1
H23 : xval V1
H24 : sexp nil (sb (rep n1 V1 :: S1) (E7 n1))
H25 : force nil (sb (rep n1 V1 :: S1) (E7 n1)) (E'1 V2)
H26 : force nil (V3 n1) V'
H27 : ees (sb (rep n1 V1 :: S1) (E7 n1)) (V3 n1)
============================
 exists V, force nil V V' /\ ees (sb S (app E5 E6)) V

eval_ees < search.
Proof completed.
Abella < Theorem force_bij_exst : 
forall H E, sexp H (sb nil E) -> force H (sb nil E) E.


============================
 forall H E, sexp H (sb nil E) -> force H (sb nil E) E

force_bij_exst < induction on 1.

IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
============================
 forall H E, sexp H (sb nil E) @ -> force H (sb nil E) E

force_bij_exst < intros.

Variables: H E
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H1 : sexp H (sb nil E) @
============================
 force H (sb nil E) E

force_bij_exst < case H1.
Subgoal 1:

Variables: H
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : vals (H n1)
H3 : sub nil *
H4 : member (val n1) (H n1)
============================
 force (H n1) (sb nil n1) n1

Subgoal 2 is:
 force (H n1) (sb nil n1) n1

Subgoal 3 is:
 force H (sb nil (num N)) (num N)

Subgoal 4 is:
 force H (sb nil (plus E1 E2)) (plus E1 E2)

Subgoal 5 is:
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < search.
Subgoal 2:

Variables: H V
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : vals (H n1)
H3 : sub nil *
H4 : member (rep n1 (V n1)) nil
============================
 force (H n1) (sb nil n1) n1

Subgoal 3 is:
 force H (sb nil (num N)) (num N)

Subgoal 4 is:
 force H (sb nil (plus E1 E2)) (plus E1 E2)

Subgoal 5 is:
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < case H4.
Subgoal 3:

Variables: H N
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : vals H
H3 : sub nil *
H4 : {natural N}
============================
 force H (sb nil (num N)) (num N)

Subgoal 4 is:
 force H (sb nil (plus E1 E2)) (plus E1 E2)

Subgoal 5 is:
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < search.
Subgoal 4:

Variables: H E2 E1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : sexp H (sb nil E1) *
H3 : sexp H (sb nil E2) *
============================
 force H (sb nil (plus E1 E2)) (plus E1 E2)

Subgoal 5 is:
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < apply IH to H2.
Subgoal 4:

Variables: H E2 E1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : sexp H (sb nil E1) *
H3 : sexp H (sb nil E2) *
H4 : force H (sb nil E1) E1
============================
 force H (sb nil (plus E1 E2)) (plus E1 E2)

Subgoal 5 is:
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < apply IH to H3.
Subgoal 4:

Variables: H E2 E1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : sexp H (sb nil E1) *
H3 : sexp H (sb nil E2) *
H4 : force H (sb nil E1) E1
H5 : force H (sb nil E2) E2
============================
 force H (sb nil (plus E1 E2)) (plus E1 E2)

Subgoal 5 is:
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < search.
Subgoal 5:

Variables: H E2 T1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : {typ T1}
H3 : sexp (val n1 :: H) (sb nil (E2 n1)) *
============================
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < apply IH to H3.
Subgoal 5:

Variables: H E2 T1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : {typ T1}
H3 : sexp (val n1 :: H) (sb nil (E2 n1)) *
H4 : force (val n1 :: H) (sb nil (E2 n1)) (E2 n1)
============================
 force H (sb nil (lam T1 E2)) (lam T1 E2)

Subgoal 6 is:
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < search.
Subgoal 6:

Variables: H E2 E1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : sexp H (sb nil E1) *
H3 : sexp H (sb nil E2) *
============================
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < apply IH to H2.
Subgoal 6:

Variables: H E2 E1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : sexp H (sb nil E1) *
H3 : sexp H (sb nil E2) *
H4 : force H (sb nil E1) E1
============================
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < apply IH to H3.
Subgoal 6:

Variables: H E2 E1
IH : forall H E, sexp H (sb nil E) * -> force H (sb nil E) E
H2 : sexp H (sb nil E1) *
H3 : sexp H (sb nil E2) *
H4 : force H (sb nil E1) E1
H5 : force H (sb nil E2) E2
============================
 force H (sb nil (app E1 E2)) (app E1 E2)

force_bij_exst < search.
Proof completed.
Abella < Theorem force_bij_uniq : 
forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 ->
  force H (sb nil E) E2 -> E1 =
E2.


============================
 forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 ->
   force H (sb nil E) E2 -> E1 =
 E2

force_bij_uniq < induction on 2.

IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
============================
 forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 @ ->
   force H (sb nil E) E2 -> E1 =
 E2

force_bij_uniq < intros.

Variables: H E E1 E2
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil E)
H2 : force H (sb nil E) E1 @
H3 : force H (sb nil E) E2
============================
 E1 = E2

force_bij_uniq < case H2.
Subgoal 1:

Variables: H E2
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp (H n1) (sb nil n1)
H3 : force (H n1) (sb nil n1) (E2 n1)
H4 : member (val n1) (H n1)
============================
 n1 = E2 n1

Subgoal 2 is:
 V' = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E1' E2' = E2

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H3.
Subgoal 1.1:

Variables: H
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp (H n1) (sb nil n1)
H4 : member (val n1) (H n1)
H5 : member (val n1) (H n1)
============================
 n1 = n1

Subgoal 1.2 is:
 n1 = V'

Subgoal 2 is:
 V' = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E1' E2' = E2

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < search.
Subgoal 1.2:

Variables: H V V'
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp (H n1) (sb nil n1)
H4 : member (val n1) (H n1)
H5 : member (rep n1 V) nil
H6 : force nil V V'
============================
 n1 = V'

Subgoal 2 is:
 V' = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E1' E2' = E2

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H5.
Subgoal 2:

Variables: H E2 V V'
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp (H n1) (sb nil n1)
H3 : force (H n1) (sb nil n1) (E2 n1)
H4 : member (rep n1 V) nil
H5 : force nil V V' *
============================
 V' = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E1' E2' = E2

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H4.
Subgoal 3:

Variables: H E2 N
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (num N))
H3 : force H (sb nil (num N)) E2
============================
 num N = E2

Subgoal 4 is:
 plus E1' E2' = E2

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H3.
Subgoal 3:

Variables: H N
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (num N))
============================
 num N = num N

Subgoal 4 is:
 plus E1' E2' = E2

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < search.
Subgoal 4:

Variables: H E2 E2' E1' E4 E3
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (plus E3 E4))
H3 : force H (sb nil (plus E3 E4)) E2
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
============================
 plus E1' E2' = E2

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H3.
Subgoal 4:

Variables: H E2' E1' E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (plus E3 E4))
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
============================
 plus E1' E2' = plus E1'1 E2'1

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H1.
Subgoal 4:

Variables: H E2' E1' E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
H8 : sexp H (sb nil E3)
H9 : sexp H (sb nil E4)
============================
 plus E1' E2' = plus E1'1 E2'1

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < apply IH to H8 H4 H6.
Subgoal 4:

Variables: H E2' E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force H (sb nil E3) E1'1 *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
H8 : sexp H (sb nil E3)
H9 : sexp H (sb nil E4)
============================
 plus E1'1 E2' = plus E1'1 E2'1

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < apply IH to H9 H5 H7.
Subgoal 4:

Variables: H E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force H (sb nil E3) E1'1 *
H5 : force H (sb nil E4) E2'1 *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
H8 : sexp H (sb nil E3)
H9 : sexp H (sb nil E4)
============================
 plus E1'1 E2'1 = plus E1'1 E2'1

Subgoal 5 is:
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < search.
Subgoal 5:

Variables: H E2 E2' T1 E3
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (lam T1 E3))
H3 : force H (sb nil (lam T1 E3)) E2
H4 : force (val n1 :: H) (sb nil (E3 n1)) (E2' n1) *
============================
 lam T1 E2' = E2

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H3.
Subgoal 5:

Variables: H E2' T1 E3 E2'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (lam T1 E3))
H4 : force (val n1 :: H) (sb nil (E3 n1)) (E2' n1) *
H5 : force (val n1 :: H) (sb nil (E3 n1)) (E2'1 n1)
============================
 lam T1 E2' = lam T1 E2'1

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < case H1.
Subgoal 5:

Variables: H E2' T1 E3 E2'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force (val n1 :: H) (sb nil (E3 n1)) (E2' n1) *
H5 : force (val n1 :: H) (sb nil (E3 n1)) (E2'1 n1)
H6 : {typ T1}
H7 : sexp (val n1 :: H) (sb nil (E3 n1))
============================
 lam T1 E2' = lam T1 E2'1

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < apply IH to H7 H4 H5.
Subgoal 5:

Variables: H T1 E3 E2'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force (val n1 :: H) (sb nil (E3 n1)) (E2'1 n1) *
H5 : force (val n1 :: H) (sb nil (E3 n1)) (E2'1 n1)
H6 : {typ T1}
H7 : sexp (val n1 :: H) (sb nil (E3 n1))
============================
 lam T1 (z1\E2'1 z1) = lam T1 E2'1

Subgoal 6 is:
 app E1' E2' = E2

force_bij_uniq < search.
Subgoal 6:

Variables: H E2 E2' E1' E4 E3
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (app E3 E4))
H3 : force H (sb nil (app E3 E4)) E2
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
============================
 app E1' E2' = E2

force_bij_uniq < case H3.
Subgoal 6:

Variables: H E2' E1' E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H1 : sexp H (sb nil (app E3 E4))
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
============================
 app E1' E2' = app E1'1 E2'1

force_bij_uniq < case H1.
Subgoal 6:

Variables: H E2' E1' E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
H8 : sexp H (sb nil E3)
H9 : sexp H (sb nil E4)
============================
 app E1' E2' = app E1'1 E2'1

force_bij_uniq < apply IH to H8 H4 H6.
Subgoal 6:

Variables: H E2' E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force H (sb nil E3) E1'1 *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
H8 : sexp H (sb nil E3)
H9 : sexp H (sb nil E4)
============================
 app E1'1 E2' = app E1'1 E2'1

force_bij_uniq < apply IH to H9 H5 H7.
Subgoal 6:

Variables: H E4 E3 E2'1 E1'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E) E1 * ->
       force H (sb nil E) E2 -> E1 =
     E2
H4 : force H (sb nil E3) E1'1 *
H5 : force H (sb nil E4) E2'1 *
H6 : force H (sb nil E3) E1'1
H7 : force H (sb nil E4) E2'1
H8 : sexp H (sb nil E3)
H9 : sexp H (sb nil E4)
============================
 app E1'1 E2'1 = app E1'1 E2'1

force_bij_uniq < search.
Proof completed.
Abella < Theorem force_bij_uniq' : 
forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E ->
  force H (sb nil E2) E -> E1 =
E2.


============================
 forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E ->
   force H (sb nil E2) E -> E1 =
 E2

force_bij_uniq' < induction on 2.

IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
============================
 forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E @ ->
   force H (sb nil E2) E -> E1 =
 E2

force_bij_uniq' < intros.

Variables: H E E1 E2
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil E)
H2 : force H (sb nil E1) E @
H3 : force H (sb nil E2) E
============================
 E1 = E2

force_bij_uniq' < case H2.
Subgoal 1:

Variables: H E2
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n1) (sb nil n1)
H3 : force (H n1) (sb nil (E2 n1)) n1
H4 : member (val n1) (H n1)
============================
 n1 = E2 n1

Subgoal 2 is:
 n1 = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H3.
Subgoal 1.1:

Variables: H
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n1) (sb nil n1)
H4 : member (val n1) (H n1)
H5 : member (val n1) (H n1)
============================
 n1 = n1

Subgoal 1.2 is:
 n1 = n2

Subgoal 2 is:
 n1 = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < search.
Subgoal 1.2:

Variables: H V
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n2 n1) (sb nil n1)
H4 : member (val n1) (H n2 n1)
H5 : member (rep n2 (V n1)) nil
H6 : force nil (V n1) n1
============================
 n1 = n2

Subgoal 2 is:
 n1 = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H5.
Subgoal 2:

Variables: H E2 V V'
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n1) (sb nil V')
H3 : force (H n1) (sb nil (E2 n1)) V'
H4 : member (rep n1 V) nil
H5 : force nil V V' *
============================
 n1 = E2 n1

Subgoal 3 is:
 num N = E2

Subgoal 4 is:
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H4.
Subgoal 3:

Variables: H E2 N
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (num N))
H3 : force H (sb nil E2) (num N)
============================
 num N = E2

Subgoal 4 is:
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H3.
Subgoal 3.1:

Variables: H N V
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n1) (sb nil (num N))
H4 : member (rep n1 V) nil
H5 : force nil V (num N)
============================
 num N = n1

Subgoal 3.2 is:
 num N = num N

Subgoal 4 is:
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H4.
Subgoal 3.2:

Variables: H N
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (num N))
============================
 num N = num N

Subgoal 4 is:
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < search.
Subgoal 4:

Variables: H E2 E2' E1' E4 E3
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (plus E1' E2'))
H3 : force H (sb nil E2) (plus E1' E2')
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
============================
 plus E3 E4 = E2

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H3.
Subgoal 4.1:

Variables: H E4 E3 V V'2 V'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n1) (sb nil (plus V'1 V'2))
H4 : force (H n1) (sb nil (E3 n1)) V'1 *
H5 : force (H n1) (sb nil (E4 n1)) V'2 *
H6 : member (rep n1 V) nil
H7 : force nil V (plus V'1 V'2)
============================
 plus (E3 n1) (E4 n1) = n1

Subgoal 4.2 is:
 plus E3 E4 = plus E5 E6

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H6.
Subgoal 4.2:

Variables: H E2' E1' E4 E3 E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (plus E1' E2'))
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
============================
 plus E3 E4 = plus E5 E6

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H1.
Subgoal 4.2:

Variables: H E2' E1' E4 E3 E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
H8 : sexp H (sb nil E1')
H9 : sexp H (sb nil E2')
============================
 plus E3 E4 = plus E5 E6

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < apply IH to H8 H4 H6.
Subgoal 4.2:

Variables: H E2' E1' E4 E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force H (sb nil E5) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
H8 : sexp H (sb nil E1')
H9 : sexp H (sb nil E2')
============================
 plus E5 E4 = plus E5 E6

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < apply IH to H9 H5 H7.
Subgoal 4.2:

Variables: H E2' E1' E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force H (sb nil E5) E1' *
H5 : force H (sb nil E6) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
H8 : sexp H (sb nil E1')
H9 : sexp H (sb nil E2')
============================
 plus E5 E6 = plus E5 E6

Subgoal 5 is:
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < search.
Subgoal 5:

Variables: H E2 E2' T1 E3
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (lam T1 E2'))
H3 : force H (sb nil E2) (lam T1 E2')
H4 : force (val n1 :: H) (sb nil (E3 n1)) (E2' n1) *
============================
 lam T1 E3 = E2

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H3.
Subgoal 5.1:

Variables: H T1 E3 V V'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n2) (sb nil (lam T1 V'1))
H4 : force (val n1 :: H n2) (sb nil (E3 n2 n1)) (V'1 n1) *
H5 : member (rep n1 V) nil
H6 : force nil V (lam T1 V'1)
============================
 lam T1 (E3 n2) = n2

Subgoal 5.2 is:
 lam T1 E3 = lam T1 E4

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H5.
Subgoal 5.2:

Variables: H E2' T1 E3 E4
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (lam T1 E2'))
H4 : force (val n1 :: H) (sb nil (E3 n1)) (E2' n1) *
H5 : force (val n1 :: H) (sb nil (E4 n1)) (E2' n1)
============================
 lam T1 E3 = lam T1 E4

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < case H1.
Subgoal 5.2:

Variables: H E2' T1 E3 E4
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force (val n1 :: H) (sb nil (E3 n1)) (E2' n1) *
H5 : force (val n1 :: H) (sb nil (E4 n1)) (E2' n1)
H6 : {typ T1}
H7 : sexp (val n1 :: H) (sb nil (E2' n1))
============================
 lam T1 E3 = lam T1 E4

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < apply IH to H7 H4 H5.
Subgoal 5.2:

Variables: H E2' T1 E4
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force (val n1 :: H) (sb nil (E4 n1)) (E2' n1) *
H5 : force (val n1 :: H) (sb nil (E4 n1)) (E2' n1)
H6 : {typ T1}
H7 : sexp (val n1 :: H) (sb nil (E2' n1))
============================
 lam T1 (z1\E4 z1) = lam T1 E4

Subgoal 6 is:
 app E3 E4 = E2

force_bij_uniq' < search.
Subgoal 6:

Variables: H E2 E2' E1' E4 E3
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (app E1' E2'))
H3 : force H (sb nil E2) (app E1' E2')
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
============================
 app E3 E4 = E2

force_bij_uniq' < case H3.
Subgoal 6.1:

Variables: H E4 E3 V V'2 V'1
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp (H n1) (sb nil (app V'1 V'2))
H4 : force (H n1) (sb nil (E3 n1)) V'1 *
H5 : force (H n1) (sb nil (E4 n1)) V'2 *
H6 : member (rep n1 V) nil
H7 : force nil V (app V'1 V'2)
============================
 app (E3 n1) (E4 n1) = n1

Subgoal 6.2 is:
 app E3 E4 = app E5 E6

force_bij_uniq' < case H6.
Subgoal 6.2:

Variables: H E2' E1' E4 E3 E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H1 : sexp H (sb nil (app E1' E2'))
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
============================
 app E3 E4 = app E5 E6

force_bij_uniq' < case H1.
Subgoal 6.2:

Variables: H E2' E1' E4 E3 E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force H (sb nil E3) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
H8 : sexp H (sb nil E1')
H9 : sexp H (sb nil E2')
============================
 app E3 E4 = app E5 E6

force_bij_uniq' < apply IH to H8 H4 H6.
Subgoal 6.2:

Variables: H E2' E1' E4 E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force H (sb nil E5) E1' *
H5 : force H (sb nil E4) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
H8 : sexp H (sb nil E1')
H9 : sexp H (sb nil E2')
============================
 app E5 E4 = app E5 E6

force_bij_uniq' < apply IH to H9 H5 H7.
Subgoal 6.2:

Variables: H E2' E1' E6 E5
IH : forall H E E1 E2, sexp H (sb nil E) -> force H (sb nil E1) E * ->
       force H (sb nil E2) E -> E1 =
     E2
H4 : force H (sb nil E5) E1' *
H5 : force H (sb nil E6) E2' *
H6 : force H (sb nil E5) E1'
H7 : force H (sb nil E6) E2'
H8 : sexp H (sb nil E1')
H9 : sexp H (sb nil E2')
============================
 app E5 E6 = app E5 E6

force_bij_uniq' < search.
Proof completed.
Abella <