proposition: Lemma equiv_eva s t : lambda t -> s == t -> exists n, eva n s = Some t.
proof: Proof. intros lt A. cut (eval s t). intros H. eapply eval_seval in H. destruct H as [n H]. eapply seval_eva in H. eauto. eauto using equiv_lambda. Qed.
imports: Coq.Logic.ConstructiveEpsilon