proposition: Lemma ord'_elements n Gamma: (forall A, A ∈ Gamma -> ord A <= n) <-> ord' Gamma <= n.
proof: Proof. induction Gamma; cbn; intuition idtac; subst; trivial. all: simplify in *; intuition auto using Nat.le_0_l. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)