proposition: Lemma eval_seval s t : eval s t -> exists n, seval n s t.
proof: Proof. intros [A B]. induction A. - destruct B. subst. eauto using seval. - destruct (IHA B) as [k C]. eauto using seval, eval_step. Unshelve. exact 0. Qed.
imports: Coq.Logic.ConstructiveEpsilon