proposition: Lemma normal_AppL_left S t: normal (AppL S t) -> Normal (lstep step) S.
proof: Proof. induction S; cbn; intros H ? H1; inv H1. - eapply H; (eauto 2). - eapply IHS; eauto using normal_app_r. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)