proposition: Lemma ordertyping_monotone m n Gamma s A: m <= n -> Gamma ⊢(m) s : A -> Gamma ⊢(n) s: A.
proof: Proof. induction 1; eauto using ordertyping_step. Qed.
imports: List Arith Lia Undecidability.HOU(std.std) Undecidability.HOU.calculus(prelim terms syntax semantics typing)