proposition: Lemma E_evaluates (s: X): { n: nat | exists t, E rho D n s = Some t } -> { t | evaluates R s t }.
proof: Proof. Proof using H1 H2 S tf refl. intros [n H]. destruct (E rho D n s) as [t|] eqn: H3. - exists t. eapply E_correct; eauto using red_fun_rho. - exfalso. destruct H. discriminate. Qed.
imports: Morphisms FinFun ConstructiveEpsilon Undecidability.HOU(std.tactics std.decidable std.misc std.ars.basic std.ars.confluence)