proposition: Lemma evaluates_E s: (exists t, evaluates R s t) -> exists n, exists t, E rho D n s = Some t.
proof: Proof. Proof using H1 H2 S tf refl. intros [t H]; destruct (E_correct red_fun_rho D s t) as [H3 _]. eapply H3 in H. destruct H as [n]. exists n. now (exists t). Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)