proposition: Lemma normal_AppR_right s T: normal (AppR s T) -> Normal (lstep step) T.
proof: Proof. induction T; cbn; intros H ? H1; inv H1. - eapply H. eauto. - eapply IHT; eauto using normal_app_l. Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)