proposition: Lemma normal_lam_intro s: normal s -> normal (lambda s).
proof: Proof. intros H1 t H2; inv H2; eapply H1; eauto. Qed.
imports: Undecidability.HOU(calculus.prelim calculus.terms calculus.syntax std.std) Morphisms Lia FinFun