proposition: Lemma steps_app_atom s t v: isAtom s -> s t >* v -> exists t', v = s t' /\ t >* t'.
proof: Proof. destruct s; intros ? [(? & ? & ? & ?)|(? & ? & ?)] % steps_app; cbn in *; intuition. all: inv H2; eauto; inv H1. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun