proposition: Lemma eval_step s s' t n : s ≻ s' -> seval n s' t -> seval (S n) s t.
proof: Proof. Proof with eauto using seval_S, seval. intros H; revert n t; induction H; intros n u A... - inv A... - inv A... Qed.
imports: Coq.Logic.ConstructiveEpsilon