proposition: Theorem systemunification_step n: 1 <= n -> @SOU X n ⪯ @SOU X (S n).
proof: Proof. intros H; exists SU_monotone; split; eauto using SU_monotone_forward, SU_monotone_backward. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)