proposition: Lemma unification_constants_monotone n: 1 <= n -> OU n X ⪯ OU n Y.
proof: Proof. Proof using re inj consts_agree RE. intros H; exists unification_retract. intros I; split; auto using unification_retract_forward, unification_retract_backward. Qed.
imports: List Arith Lia Morphisms Setoid Undecidability.HOU(calculus.calculus) Undecidability.HOU(unification.higher_order_unification unification.nth_order_unification concon.conservativity_constants concon.conservativity)