proposition: Lemma steps_app s t v: app s t >* v -> (exists s', exists t', v = app s' t' /\ s >* s' /\ t >* t') \/ (exists s', s >* lambda s' /\ isLam (head s)).
proof: Proof. remember (s t) as r. intros H1. revert s t Heqr. induction H1. - intros; subst. left; eexists; eexists; intuition. - intros; subst. inv H. + right. eexists; split; cbn; eauto. + edestruct IHstar; eauto. * destruct H as (? & ? & ? & ? & ?); subst. left. eexists; eexists; eauto. * destruct H as (? & ? & ?). right. eexists; split; eauto. eapply head_preserved; eauto. + edestruct IHstar; eauto. * destruct H as (? & ? & ? & ? & ?); subst. left. eexists; eexists; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun