proposition: Lemma normal_app_not_lam s t: normal (s t) -> ~ isLam s.
proof: Proof. destruct s; intuition; eapply H; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun