proposition: Lemma ord'_in A Gamma: A ∈ Gamma -> ord A <= ord' Gamma.
proof: Proof. induction Gamma; cbn in *; intuition idtac; subst; auto; lia. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)