proposition: Lemma eqs_ordertyping_monotone Gamma n m E L: n <= m -> Gamma ⊢₊₊(n) E : L -> Gamma ⊢₊₊(m) E : L.
proof: Proof. induction 1; eauto using eqs_ordertyping_step. Qed.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)