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