proposition: Lemma eval_iff s t : L.eval s t <-> s ⇓ t.
proof: Proof. split. - induction 1. + split. reflexivity. eauto. + split. destruct IHeval2 as [IH1 [v' ->]]. 2:eapply IHeval3. rewrite IHeval1, IH1. econstructor. 2:eapply IHeval3. econstructor. - intros [H1 [v ->]]. revert H1. revert s. eapply (star_simpl_ind (y := lam v)). + econstructor. + intros s s' H1 H2 IH. eapply step_eval; eauto. Qed.
imports: Lia