proposition: Lemma steps_lam s v: lambda s >* v -> exists s', v = lambda s' /\ s >* s'.
proof: Proof. remember (lambda s) as t. intros H1. revert s Heqt. induction H1. - intros ? ->; eexists; eauto. - intros; subst. inv H. edestruct IHstar; eauto; intuition; subst. exists x. eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun