proposition: Lemma typing_Consts X c n Gamma S' L: Gamma ⊢₊(n) S' : L -> c ∈ Consts S' -> ord (ctype X c) <= S n.
proof: Proof. induction 1; cbn; simplify; intuition eauto using typing_constants. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)