proposition: Lemma ord'_cons n Gamma A: ord A < n -> ord' Gamma <= n -> ord' (A :: Gamma) <= n.
proof: Proof. intros; cbn; eapply Nat.max_lub; lia. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)