proposition: Lemma seval_Eval n (s t:term): seval n s t -> Eval (ext s) == (ext t).
proof: Proof. intros. apply seval_eva in H. rewrite Eval_correct;try Lproc. exists n,t. repeat split. - Lsimpl. rewrite H. reflexivity. - apply eva_lam in H. Lproc. Qed.