proposition: Theorem unification_step n: 1 <= n -> OU n X ⪯ OU (S n) X.
proof: Proof. intros H; exists unification_monotone; split; eauto using unification_monotone_forward, unification_monotone_backward. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)