proposition: Lemma eva_lam n s t : eva n s = Some t -> lambda t.
proof: Proof. revert s t; induction n; intros s t H; destruct s; try inv H; eauto. destruct (eva n s1) eqn:Hs1; try now inv H1. destruct t0; try inv H1. destruct (eva n s2); try inv H0. eapply IHn in H1. eassumption. Qed.
imports: Coq.Logic.ConstructiveEpsilon