proposition: Lemma AppL_ordertyping_repeated k Gamma s T n A: Gamma ⊢₊(n) T: repeat (A → A) k -> Gamma ⊢(n) s : A -> Gamma ⊢(n) AppL T s : A.
proof: Proof. induction T in k |-*; (eauto 1); cbn. intros; inv H; intuition. destruct k; try discriminate. cbn in H3; injection H3 as ??; subst. econstructor; (eauto 2). Qed.
imports: List Arith Lia Morphisms FinFun Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics equivalence typing order confluence)