proposition: Lemma Eval_eval (s t : term) : lambda t -> Eval (ext s) == t -> exists t', ext t' = t /\ eval s t'.
proof: Proof. Proof with Lproc. intros p H. rewrite Eval_correct in H;try Lproc. destruct H as [n [v [R [eq lv]]]]. subst t. eexists. split. reflexivity. Lrewrite in R. apply enc_extinj in R. apply eva_equiv in R. split. apply equiv_lambda;try Lproc. assumption. assumption. Qed.