proposition: Lemma normal_app_intro s t: ~ isLam s -> normal s -> normal t -> normal (s t).
proof: Proof. intros; intros t' H2; inv H2; cbn in *; eauto. all: firstorder. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun