Welcome to Abella 2.0.5-dev.
```Abella < Specification "eval".

```
```Abella < Theorem eval_det :
forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2.

```
```
============================
forall E V1 V2, {eval E V1} -> {eval E V2} -> V1 = V2

eval_det < induction on 1.
```
```
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
============================
forall E V1 V2, {eval E V1}@ -> {eval E V2} -> V1 = V2

eval_det < intros.
```
```
Variables: E V1 V2
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H1 : {eval E V1}@
H2 : {eval E V2}
============================
V1 = V2

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

Variables: V2 R
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H2 : {eval (abs R) V2}
============================
abs R = V2

Subgoal 2 is:
V1 = V2

eval_det < case H2.
```
```Subgoal 1:

Variables: R
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
============================
abs R = abs R

Subgoal 2 is:
V1 = V2

eval_det < search.
```
```Subgoal 2:

Variables: V1 V2 N R M
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H2 : {eval (app M N) V2}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V1}*
============================
V1 = V2

eval_det < case H2.
```
```Subgoal 2:

Variables: V1 V2 N R M R1
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H3 : {eval M (abs R)}*
H4 : {eval (R N) V1}*
H5 : {eval M (abs R1)}
H6 : {eval (R1 N) V2}
============================
V1 = V2

eval_det < apply IH to H3 H5.
```
```Subgoal 2:

Variables: V1 V2 N M R1
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H3 : {eval M (abs R1)}*
H4 : {eval (R1 N) V1}*
H5 : {eval M (abs R1)}
H6 : {eval (R1 N) V2}
============================
V1 = V2

eval_det < apply IH to H4 H6.
```
```Subgoal 2:

Variables: V2 N M R1
IH : forall E V1 V2, {eval E V1}* -> {eval E V2} -> V1 = V2
H3 : {eval M (abs R1)}*
H4 : {eval (R1 N) V2}*
H5 : {eval M (abs R1)}
H6 : {eval (R1 N) V2}
============================
V2 = V2

eval_det < search.
Proof completed.
```
```Abella < Theorem step_det :
forall E1 E2 E3, {step E1 E2} -> {step E1 E3} -> E2 = E3.

```
```
============================
forall E1 E2 E3, {step E1 E2} -> {step E1 E3} -> E2 = E3

step_det < induction on 1.
```
```
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
============================
forall E1 E2 E3, {step E1 E2}@ -> {step E1 E3} -> E2 = E3

step_det < intros.
```
```
Variables: E1 E2 E3
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H1 : {step E1 E2}@
H2 : {step E1 E3}
============================
E2 = E3

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

Variables: E3 M R
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H2 : {step (app (abs R) M) E3}
============================
R M = E3

Subgoal 2 is:
app M' N = E3

step_det < case H2.
```
```Subgoal 1.1:

Variables: M R
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
============================
R M = R M

Subgoal 1.2 is:
R M = app M' M

Subgoal 2 is:
app M' N = E3

step_det < search.
```
```Subgoal 1.2:

Variables: M R M'
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step (abs R) M'}
============================
R M = app M' M

Subgoal 2 is:
app M' N = E3

step_det < case H3.
```
```Subgoal 2:

Variables: E3 M' M N
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H2 : {step (app M N) E3}
H3 : {step M M'}*
============================
app M' N = E3

step_det < case H2.
```
```Subgoal 2.1:

Variables: M' N R
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step (abs R) M'}*
============================
app M' N = R N

Subgoal 2.2 is:
app M' N = app M'1 N

step_det < case H3.
```
```Subgoal 2.2:

Variables: M' M N M'1
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step M M'}*
H4 : {step M M'1}
============================
app M' N = app M'1 N

step_det < apply IH to H3 H4.
```
```Subgoal 2.2:

Variables: M N M'1
IH : forall E1 E2 E3, {step E1 E2}* -> {step E1 E3} -> E2 = E3
H3 : {step M M'1}*
H4 : {step M M'1}
============================
app M'1 N = app M'1 N

step_det < search.
Proof completed.
```
```Abella < Theorem nstep_det :
forall E R1 R2, {nstep E (abs R1)} -> {nstep E (abs R2)} -> R1 = R2.

```
```
============================
forall E R1 R2, {nstep E (abs R1)} -> {nstep E (abs R2)} -> R1 = R2

nstep_det < induction on 1.
```
```
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
============================
forall E R1 R2, {nstep E (abs R1)}@ -> {nstep E (abs R2)} -> R1 = R2

nstep_det < intros.
```
```
Variables: E R1 R2
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H1 : {nstep E (abs R1)}@
H2 : {nstep E (abs R2)}
============================
R1 = R2

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

Variables: R1 R2
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H2 : {nstep (abs R1) (abs R2)}
============================
R1 = R2

Subgoal 2 is:
R1 = R2

nstep_det < case H2.
```
```Subgoal 1.1:

Variables: R2
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
============================
R2 = R2

Subgoal 1.2 is:
R1 = R2

Subgoal 2 is:
R1 = R2

nstep_det < search.
```
```Subgoal 1.2:

Variables: R1 R2 B
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step (abs R1) B}
H4 : {nstep B (abs R2)}
============================
R1 = R2

Subgoal 2 is:
R1 = R2

nstep_det < case H3.
```
```Subgoal 2:

Variables: E R1 R2 B
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H2 : {nstep E (abs R2)}
H3 : {step E B}*
H4 : {nstep B (abs R1)}*
============================
R1 = R2

nstep_det < case H2.
```
```Subgoal 2.1:

Variables: R1 R2 B
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step (abs R2) B}*
H4 : {nstep B (abs R1)}*
============================
R1 = R2

Subgoal 2.2 is:
R1 = R2

nstep_det < case H3.
```
```Subgoal 2.2:

Variables: E R1 R2 B B1
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step E B}*
H4 : {nstep B (abs R1)}*
H5 : {step E B1}
H6 : {nstep B1 (abs R2)}
============================
R1 = R2

nstep_det < apply step_det to H3 H5.
```
```Subgoal 2.2:

Variables: E R1 R2 B1
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step E B1}*
H4 : {nstep B1 (abs R1)}*
H5 : {step E B1}
H6 : {nstep B1 (abs R2)}
============================
R1 = R2

nstep_det < apply IH to H4 H6.
```
```Subgoal 2.2:

Variables: E R2 B1
IH : forall E R1 R2, {nstep E (abs R1)}* -> {nstep E (abs R2)} -> R1 = R2
H3 : {step E B1}*
H4 : {nstep B1 (abs R2)}*
H5 : {step E B1}
H6 : {nstep B1 (abs R2)}
============================
R2 = R2

nstep_det < search.
Proof completed.
```
```Abella < Theorem nstep_lemma :
forall M N R V, {nstep M (abs R)} -> {nstep (R N) V} -> {nstep (app M N) V}.

```
```
============================
forall M N R V, {nstep M (abs R)} -> {nstep (R N) V} -> {nstep (app M N) V}

nstep_lemma < induction on 1.
```
```
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
{nstep (app M N) V}
============================
forall M N R V, {nstep M (abs R)}@ -> {nstep (R N) V} -> {nstep (app M N) V}

nstep_lemma < intros.
```
```
Variables: M N R V
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
{nstep (app M N) V}
H1 : {nstep M (abs R)}@
H2 : {nstep (R N) V}
============================
{nstep (app M N) V}

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

Variables: N R V
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
{nstep (app M N) V}
H2 : {nstep (R N) V}
============================
{nstep (app (abs R) N) V}

Subgoal 2 is:
{nstep (app M N) V}

nstep_lemma < search.
```
```Subgoal 2:

Variables: M N R V B
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
{nstep (app M N) V}
H2 : {nstep (R N) V}
H3 : {step M B}*
H4 : {nstep B (abs R)}*
============================
{nstep (app M N) V}

nstep_lemma < apply IH to H4 H2.
```
```Subgoal 2:

Variables: M N R V B
IH : forall M N R V, {nstep M (abs R)}* -> {nstep (R N) V} ->
{nstep (app M N) V}
H2 : {nstep (R N) V}
H3 : {step M B}*
H4 : {nstep B (abs R)}*
H5 : {nstep (app B N) V}
============================
{nstep (app M N) V}

nstep_lemma < search.
Proof completed.
```
```Abella < Theorem eval_nstep :
forall E V, {eval E V} -> {nstep E V}.

```
```
============================
forall E V, {eval E V} -> {nstep E V}

eval_nstep < induction on 1.
```
```
IH : forall E V, {eval E V}* -> {nstep E V}
============================
forall E V, {eval E V}@ -> {nstep E V}

eval_nstep < intros.
```
```
Variables: E V
IH : forall E V, {eval E V}* -> {nstep E V}
H1 : {eval E V}@
============================
{nstep E V}

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

Variables: R
IH : forall E V, {eval E V}* -> {nstep E V}
============================
{nstep (abs R) (abs R)}

Subgoal 2 is:
{nstep (app M N) V}

eval_nstep < search.
```
```Subgoal 2:

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
============================
{nstep (app M N) V}

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

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
H4 : {nstep M (abs R)}
============================
{nstep (app M N) V}

eval_nstep < apply IH to H3.
```
```Subgoal 2:

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
H4 : {nstep M (abs R)}
H5 : {nstep (R N) V}
============================
{nstep (app M N) V}

eval_nstep < apply nstep_lemma to H4 H5.
```
```Subgoal 2:

Variables: V N R M
IH : forall E V, {eval E V}* -> {nstep E V}
H2 : {eval M (abs R)}*
H3 : {eval (R N) V}*
H4 : {nstep M (abs R)}
H5 : {nstep (R N) V}
H6 : {nstep (app M N) V}
============================
{nstep (app M N) V}

eval_nstep < search.
Proof completed.
```
```Abella < Theorem step_eval_lemma :
forall A B C, {step A B} -> {eval B C} -> {eval A C}.

```
```
============================
forall A B C, {step A B} -> {eval B C} -> {eval A C}

step_eval_lemma < induction on 1.
```
```
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
============================
forall A B C, {step A B}@ -> {eval B C} -> {eval A C}

step_eval_lemma < intros.
```
```
Variables: A B C
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H1 : {step A B}@
H2 : {eval B C}
============================
{eval A C}

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

Variables: C M R
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H2 : {eval (R M) C}
============================
{eval (app (abs R) M) C}

Subgoal 2 is:
{eval (app M N) C}

step_eval_lemma < search.
```
```Subgoal 2:

Variables: C M' M N
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H2 : {eval (app M' N) C}
H3 : {step M M'}*
============================
{eval (app M N) C}

step_eval_lemma < case H2.
```
```Subgoal 2:

Variables: C M' M N R
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H3 : {step M M'}*
H4 : {eval M' (abs R)}
H5 : {eval (R N) C}
============================
{eval (app M N) C}

step_eval_lemma < apply IH to H3 H4.
```
```Subgoal 2:

Variables: C M' M N R
IH : forall A B C, {step A B}* -> {eval B C} -> {eval A C}
H3 : {step M M'}*
H4 : {eval M' (abs R)}
H5 : {eval (R N) C}
H6 : {eval M (abs R)}
============================
{eval (app M N) C}

step_eval_lemma < search.
Proof completed.
```
```Abella < Theorem nstep_eval :
forall E R, {nstep E (abs R)} -> {eval E (abs R)}.

```
```
============================
forall E R, {nstep E (abs R)} -> {eval E (abs R)}

nstep_eval < induction on 1.
```
```
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
============================
forall E R, {nstep E (abs R)}@ -> {eval E (abs R)}

nstep_eval < intros.
```
```
Variables: E R
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H1 : {nstep E (abs R)}@
============================
{eval E (abs R)}

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

Variables: R
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
============================
{eval (abs R) (abs R)}

Subgoal 2 is:
{eval E (abs R)}

nstep_eval < search.
```
```Subgoal 2:

Variables: E R B
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H2 : {step E B}*
H3 : {nstep B (abs R)}*
============================
{eval E (abs R)}

nstep_eval < apply IH to H3.
```
```Subgoal 2:

Variables: E R B
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H2 : {step E B}*
H3 : {nstep B (abs R)}*
H4 : {eval B (abs R)}
============================
{eval E (abs R)}

nstep_eval < apply step_eval_lemma to H2 H4.
```
```Subgoal 2:

Variables: E R B
IH : forall E R, {nstep E (abs R)}* -> {eval E (abs R)}
H2 : {step E B}*
H3 : {nstep B (abs R)}*
H4 : {eval B (abs R)}
H5 : {eval E (abs R)}
============================
{eval E (abs R)}

nstep_eval < search.
Proof completed.
```
```Abella < Theorem sr_eval :
forall E V T, {eval E V} -> {of E T} -> {of V T}.

```
```
============================
forall E V T, {eval E V} -> {of E T} -> {of V T}

sr_eval < induction on 1.
```
```
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
============================
forall E V T, {eval E V}@ -> {of E T} -> {of V T}

sr_eval < intros.
```
```
Variables: E V T
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H1 : {eval E V}@
H2 : {of E T}
============================
{of V T}

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

Variables: T R
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H2 : {of (abs R) T}
============================
{of (abs R) T}

Subgoal 2 is:
{of V T}

sr_eval < search.
```
```Subgoal 2:

Variables: V T N R M
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H2 : {of (app M N) T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
============================
{of V T}

sr_eval < case H2.
```
```Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
============================
{of V T}

sr_eval < apply IH to H3 H5.
```
```Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H7 : {of (abs R) (arrow U T)}
============================
{of V T}

sr_eval < case H7.
```
```Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
============================
{of V T}

sr_eval <  inst H8 with n1 = N.
```
```Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
H9 : {of N U |- of (R N) T}
============================
{of V T}

sr_eval < cut H9 with H6.
```
```Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
H9 : {of N U |- of (R N) T}
H10 : {of (R N) T}
============================
{of V T}

sr_eval < apply IH to H4 H10.
```
```Subgoal 2:

Variables: V T N R M U
IH : forall E V T, {eval E V}* -> {of E T} -> {of V T}
H3 : {eval M (abs R)}*
H4 : {eval (R N) V}*
H5 : {of M (arrow U T)}
H6 : {of N U}
H8 : {of n1 U |- of (R n1) T}
H9 : {of N U |- of (R N) T}
H10 : {of (R N) T}
H11 : {of V T}
============================
{of V T}

sr_eval < search.
Proof completed.
```
```Abella < Theorem sr_step :
forall E1 E2 T, {step E1 E2} -> {of E1 T} -> {of E2 T}.

```
```
============================
forall E1 E2 T, {step E1 E2} -> {of E1 T} -> {of E2 T}

sr_step < induction on 1.
```
```
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
============================
forall E1 E2 T, {step E1 E2}@ -> {of E1 T} -> {of E2 T}

sr_step < intros.
```
```
Variables: E1 E2 T
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H1 : {step E1 E2}@
H2 : {of E1 T}
============================
{of E2 T}

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

Variables: T M R
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of (app (abs R) M) T}
============================
{of (R M) T}

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

sr_step < case H2.
```
```Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H3 : {of (abs R) (arrow U T)}
H4 : {of M U}
============================
{of (R M) T}

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

sr_step < case H3.
```
```Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H4 : {of M U}
H5 : {of n1 U |- of (R n1) T}
============================
{of (R M) T}

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

sr_step <  inst H5 with n1 = M.
```
```Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H4 : {of M U}
H5 : {of n1 U |- of (R n1) T}
H6 : {of M U |- of (R M) T}
============================
{of (R M) T}

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

sr_step < cut H6 with H4.
```
```Subgoal 1:

Variables: T M R U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H4 : {of M U}
H5 : {of n1 U |- of (R n1) T}
H6 : {of M U |- of (R M) T}
H7 : {of (R M) T}
============================
{of (R M) T}

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

sr_step < search.
```
```Subgoal 2:

Variables: T M' M N
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of (app M N) T}
H3 : {step M M'}*
============================
{of (app M' N) T}

sr_step < case H2.
```
```Subgoal 2:

Variables: T M' M N U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H3 : {step M M'}*
H4 : {of M (arrow U T)}
H5 : {of N U}
============================
{of (app M' N) T}

sr_step < apply IH to H3 H4.
```
```Subgoal 2:

Variables: T M' M N U
IH : forall E1 E2 T, {step E1 E2}* -> {of E1 T} -> {of E2 T}
H3 : {step M M'}*
H4 : {of M (arrow U T)}
H5 : {of N U}
H6 : {of M' (arrow U T)}
============================
{of (app M' N) T}

sr_step < search.
Proof completed.
```
```Abella < Theorem sr_nstep :
forall E1 E2 T, {nstep E1 E2} -> {of E1 T} -> {of E2 T}.

```
```
============================
forall E1 E2 T, {nstep E1 E2} -> {of E1 T} -> {of E2 T}

sr_nstep < induction on 1.
```
```
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
============================
forall E1 E2 T, {nstep E1 E2}@ -> {of E1 T} -> {of E2 T}

sr_nstep < intros.
```
```
Variables: E1 E2 T
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H1 : {nstep E1 E2}@
H2 : {of E1 T}
============================
{of E2 T}

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

Variables: E2 T
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E2 T}
============================
{of E2 T}

Subgoal 2 is:
{of E2 T}

sr_nstep < search.
```
```Subgoal 2:

Variables: E1 E2 T B
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E1 T}
H3 : {step E1 B}*
H4 : {nstep B E2}*
============================
{of E2 T}

sr_nstep < apply sr_step to H3 H2.
```
```Subgoal 2:

Variables: E1 E2 T B
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E1 T}
H3 : {step E1 B}*
H4 : {nstep B E2}*
H5 : {of B T}
============================
{of E2 T}

sr_nstep < apply IH to H4 H5.
```
```Subgoal 2:

Variables: E1 E2 T B
IH : forall E1 E2 T, {nstep E1 E2}* -> {of E1 T} -> {of E2 T}
H2 : {of E1 T}
H3 : {step E1 B}*
H4 : {nstep B E2}*
H5 : {of B T}
H6 : {of E2 T}
============================
{of E2 T}

sr_nstep < search.
Proof completed.
```
```Abella < Theorem type_subst :
forall L E E' T T', nabla x, {L, of x T' |- of (E x) T} -> {L |- of E' T'} ->
{L |- of (E E') T}.

```
```
============================
forall L E E' T T', nabla x, {L, of x T' |- of (E x) T} ->
{L |- of E' T'} -> {L |- of (E E') T}

type_subst < intros.
```
```
Variables: L E E' T T'
H1 : {L, of n1 T' |- of (E n1) T}
H2 : {L |- of E' T'}
============================
{L |- of (E E') T}

type_subst <  inst H1 with n1 = E'.
```
```
Variables: L E E' T T'
H1 : {L, of n1 T' |- of (E n1) T}
H2 : {L |- of E' T'}
H3 : {L, of E' T' |- of (E E') T}
============================
{L |- of (E E') T}

type_subst < cut H3 with H2.
```
```
Variables: L E E' T T'
H1 : {L, of n1 T' |- of (E n1) T}
H2 : {L |- of E' T'}
H3 : {L, of E' T' |- of (E E') T}
H4 : {L |- of (E E') T}
============================
{L |- of (E E') T}

type_subst < search.
Proof completed.
```
```Abella < Theorem of_self_app_absurd :
forall T, {of (abs (x\app x x)) T} -> false.

```
```
============================
forall T, {of (abs (x\app x x)) T} -> false

of_self_app_absurd < intros.
```
```
Variables: T
H1 : {of (abs (x\app x x)) T}
============================
false

of_self_app_absurd < case H1.
```
```
Variables: U T1
H2 : {of n1 T1 |- of (app n1 n1) U}
============================
false

of_self_app_absurd < case H2.
```
```Subgoal 1:

Variables: U T1 U1
H3 : {of n1 T1 |- of n1 (arrow (U1 n1) U)}
H4 : {of n1 T1 |- of n1 (U1 n1)}
============================
false

Subgoal 2 is:
false

of_self_app_absurd < case H3.
```
```Subgoal 1:

Variables: U T1 U1 F
H4 : {of n1 T1 |- of n1 (U1 n1)}
H5 : {of n1 T1, [F n1] |- of n1 (arrow (U1 n1) U)}
H6 : member (F n1) (of n1 T1 :: nil)
============================
false

Subgoal 2 is:
false

of_self_app_absurd < case H6.
```
```Subgoal 1.1:

Variables: U T1 U1
H4 : {of n1 T1 |- of n1 (U1 n1)}
H5 : {of n1 T1, [of n1 T1] |- of n1 (arrow (U1 n1) U)}
============================
false

Subgoal 1.2 is:
false

Subgoal 2 is:
false

of_self_app_absurd < case H5.
```
```Subgoal 1.1:

Variables: U T2
H4 : {of n1 (arrow T2 U) |- of n1 T2}
============================
false

Subgoal 1.2 is:
false

Subgoal 2 is:
false

of_self_app_absurd < case H4.
```
```Subgoal 1.1:

Variables: U T2 F1
H7 : {of n1 (arrow T2 U), [F1 n1] |- of n1 T2}
H8 : member (F1 n1) (of n1 (arrow T2 U) :: nil)
============================
false

Subgoal 1.2 is:
false

Subgoal 2 is:
false

of_self_app_absurd < case H8.
```
```Subgoal 1.1.1:

Variables: U T2
H7 : {of n1 (arrow T2 U), [of n1 (arrow T2 U)] |- of n1 T2}
============================
false

Subgoal 1.1.2 is:
false

Subgoal 1.2 is:
false

Subgoal 2 is:
false

of_self_app_absurd < case H7.
```
```Subgoal 1.1.2:

Variables: U T2 F1
H7 : {of n1 (arrow T2 U), [F1 n1] |- of n1 T2}
H9 : member (F1 n1) nil
============================
false

Subgoal 1.2 is:
false

Subgoal 2 is:
false

of_self_app_absurd < case H9.
```
```Subgoal 1.2:

Variables: U T1 U1 F
H4 : {of n1 T1 |- of n1 (U1 n1)}
H5 : {of n1 T1, [F n1] |- of n1 (arrow (U1 n1) U)}
H7 : member (F n1) nil
============================
false

Subgoal 2 is:
false

of_self_app_absurd < case H7.
```
```Subgoal 2:

Variables: U T1 F
H3 : {of n1 T1, [F n1] |- of (app n1 n1) U}
H4 : member (F n1) (of n1 T1 :: nil)
============================
false

of_self_app_absurd < case H4.
```
```Subgoal 2.1:

Variables: U T1
H3 : {of n1 T1, [of n1 T1] |- of (app n1 n1) U}
============================
false

Subgoal 2.2 is:
false

of_self_app_absurd < case H3.
```
```Subgoal 2.2:

Variables: U T1 F
H3 : {of n1 T1, [F n1] |- of (app n1 n1) U}
H5 : member (F n1) nil
============================
false

of_self_app_absurd < case H5.
Proof completed.
```
```Abella < Theorem no_eval :
forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V} -> false.

```
```
============================
forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V} -> false

no_eval < induction on 1.
```
```
IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
============================
forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}@ -> false

no_eval < intros.
```
```
Variables: V
IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
H1 : {eval (app (abs (x\app x x)) (abs (x\app x x))) V}@
============================
false

no_eval < case H1.
```
```
Variables: V R
IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
H2 : {eval (abs (x\app x x)) (abs R)}*
H3 : {eval (R (abs (x\app x x))) V}*
============================
false

no_eval < case H2.
```
```
Variables: V
IH : forall V, {eval (app (abs (x\app x x)) (abs (x\app x x))) V}* -> false
H3 : {eval (app (abs (x\app x x)) (abs (x\app x x))) V}*
============================
false

no_eval < apply IH to H3.
Proof completed.
```
```Abella < CoDefine diverge : tm -> prop by
diverge (app M N) := diverge M;
diverge (app M N) := exists R, {eval M (abs R)} /\ diverge (R N).

```
```Abella < Theorem omega_diverge :
diverge (app (abs (x\app x x)) (abs (x\app x x))).

```
```
============================
diverge (app (abs (x\app x x)) (abs (x\app x x)))

omega_diverge < coinduction.
```
```
CH : diverge (app (abs (x\app x x)) (abs (x\app x x))) +
============================
diverge (app (abs (x\app x x)) (abs (x\app x x))) #

omega_diverge < search.
Proof completed.
```
```Abella < Theorem eval_diverge_absurd :
forall M V, {eval M V} -> diverge M -> false.

```
```
============================
forall M V, {eval M V} -> diverge M -> false

eval_diverge_absurd < induction on 1.
```
```
IH : forall M V, {eval M V}* -> diverge M -> false
============================
forall M V, {eval M V}@ -> diverge M -> false

eval_diverge_absurd < intros.
```
```
Variables: M V
IH : forall M V, {eval M V}* -> diverge M -> false
H1 : {eval M V}@
H2 : diverge M
============================
false

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

Variables: R
IH : forall M V, {eval M V}* -> diverge M -> false
H2 : diverge (abs R)
============================
false

Subgoal 2 is:
false

eval_diverge_absurd < case H2.
```
```Subgoal 2:

Variables: V N R M1
IH : forall M V, {eval M V}* -> diverge M -> false
H2 : diverge (app M1 N)
H3 : {eval M1 (abs R)}*
H4 : {eval (R N) V}*
============================
false

eval_diverge_absurd < case H2.
```
```Subgoal 2.1:

Variables: V N R M1
IH : forall M V, {eval M V}* -> diverge M -> false
H3 : {eval M1 (abs R)}*
H4 : {eval (R N) V}*
H5 : diverge M1
============================
false

Subgoal 2.2 is:
false

eval_diverge_absurd < apply IH to H3 H5.
```
```Subgoal 2.2:

Variables: V N R M1 R1
IH : forall M V, {eval M V}* -> diverge M -> false
H3 : {eval M1 (abs R)}*
H4 : {eval (R N) V}*
H5 : {eval M1 (abs R1)}
H6 : diverge (R1 N)
============================
false

eval_diverge_absurd < apply eval_det to H3 H5.
```
```Subgoal 2.2:

Variables: V N M1 R1
IH : forall M V, {eval M V}* -> diverge M -> false
H3 : {eval M1 (abs R1)}*
H4 : {eval (R1 N) V}*
H5 : {eval M1 (abs R1)}
H6 : diverge (R1 N)
============================
false

eval_diverge_absurd < apply IH to H4 H6.
Proof completed.
```
```Abella <
```