proposition: Lemma seval_eval n s t : seval n s t -> eval s t.
proof: Proof. Proof with eauto using star_trans, star_trans_l, star_trans_r. intros. induction H as [ | n s t u v w _ [IHe1 _] _ [IHe2 _] _ [IHe3 lam_w]]. - repeat econstructor. - split... transitivity ((lam u) t)... transitivity ((lam u) (lam v))... now rewrite stepApp. Qed.
imports: Coq.Logic.ConstructiveEpsilon