Definition Eva := R (.\ "Eva","n","u";"u" (.\"";!none)
                                          (.\"s","t"; "n" !none
                                                          (.\"n"; "Eva" "n" "s"
                                                                   (.\"s"; "Eva" "n" "t"
                                                                            (.\"t"; "s"
                                                                                    (.\""; !none)
                                                                                    (.\"",""; !none)
                                                                                    (.\"s"; "Eva" "n" (!Subst "s" !Zero "t")))
                                                                             !none)
                                                                   !none))
                                          (.\"s"; !some (!Lam "s"))).

Lemma Eva_rec_var k n : Eva (enc k) (tenc (# n)) == none.

Lemma Eva_rec_lam k s : Eva (enc k) (tenc (lam s)) == some (Lam (tenc s)).

Lemma Eva_rec_app_0 s t : Eva Zero (tenc (app s t)) == none.

Lemma Eva_rec_app_Sn s t n :
  Eva (enc (S n)) (tenc (app s t)) == Eva (enc n) (tenc s) (lam ((lam (Eva #0)) (enc n) (tenc t) (lam (
                                                                #1 (lam none)
                                                                   (lam (lam none))
                                                                   (lam ((lam (Eva #0)) (enc n) (Subst #0 Zero #1))))) none )) none.

Definition cLam s := lam(lam(lam(#0 s))).

Lemma Eva_rec_app_Sn_1 s t n s1 t1 :
   proc s1 →
   proc t1 →
   Eva (enc n) (tenc s) == some (cLam s1) →
   Eva (enc n) (tenc t) == some (cLam t1) →
   Eva (enc (S n)) (tenc (app s t)) == Eva (enc n) (Subst s1 Zero (cLam t1)).

Lemma Eva_rec_app_Sn_2 s t n : Eva (enc n) (tenc s) == none → Eva (enc (S n)) (tenc (s t)) == none.

Lemma Eva_rec_app_Sn_3 s t n s1 t1 : proc s1
                                   → proc t1
                                   → Eva (enc n) (tenc s) == some (cLam t1)
                                   → Eva (enc n) (tenc t) == none
                                   → Eva (enc (S n)) (tenc (s t)) == none.


Lemma Eva_correct k s : Eva (enc k) (tenc s) == oenc (eva k s).

Definition Eval := Se (.\"x"; !Eva "x").




Lemma Eval_correct s v : proc v → (Eval (tenc s) == v ↔ ∃ n, Eva (enc n) (tenc s) == some v).

Lemma seval_Eval n s t: seval n s t → Eval (tenc s) == (tenc t).

Lemma eval_Eval s t : eval s t → Eval (tenc s) == (tenc t).

Lemma equiv_lambda' s t : lambda t → s == t → s >* t.

Lemma Eval_eval (s t : term) : Eval (tenc s) == tenc t → eval s t.

Lemma eval_converges s : converges s → ∃ t, eval s t.

Lemma Eval_converges s : converges s ↔ converges (Eval (tenc s)).