Definition RE P := ∃ (f : term), closed f ∧ (∀ n, f(enc n) == none ∨ ∃ s, f (enc n) == some (tenc s) ∧ P s) ∧ ∀ s, P s → ∃ n, f (enc n) == some (tenc s).

Section Fix_f.

  Variable f : term.
  Hypothesis cls_f : closed f.
  Hypothesis total_f : ∀ n, f (enc n) == none ∨ ∃ s, f (enc n) == some (tenc s).

  Definition Re := R (.\ "Re", "n", "s"; (!f "n") (.\"t"; ( !(lam(Eq #0)) "t" "s" !I (.\ "", ""; "Re" (!Succ "n") "s") !I))
                                                                     (.\ ""; "Re" (!Succ "n") "s") !I).


  Lemma Re_rec_s n t : Re (enc n) (tenc t) >* (f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc t) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc t)))) I))
                                                                   (lam ((lam(Re #0)) (Succ (enc n)) (tenc t))) I.

  Lemma Re_rec n t : Re (enc n) (tenc t) == (f (enc n)) (lam ( (lam(Eq #0)) #0 (tenc t) I (lam(lam ( (lam(Re #0)) (Succ (enc n)) (tenc t)))) I))
                                                                   (lam ((lam(Re #0)) (Succ (enc n)) (tenc t))) I.

  Lemma Re_S n s : converges (Re (enc (S n)) (tenc s)) → converges (Re (enc n) (tenc s)).

  Lemma Re_ge n m s : n ≥ m → converges (Re (enc n) (tenc s)) → converges (Re (enc m) (tenc s)).

  Lemma Re_converges n s : converges (Re (enc n) (tenc s)) → ∃ n, f (enc n) == oenc (Some s).

End Fix_f.

Lemma RE_Acc P : RE P → lacc P.

Lemma pi_eval u s : pi u s → ∃ v, eval (u (tenc s)) v.

Theorem Acc_RE P : lacc P → RE P.