proposition: Lemma typing_constants X n Gamma s A : Gamma ⊢(n) s : A -> forall c, c ∈ consts s -> ord (ctype X c) <= S n.
proof: Proof. induction 1; cbn; intuition idtac; subst; trivial. simplify in H1; intuition. Qed.
imports: Morphisms Lia List Undecidability.HOU(calculus.calculus)