proposition: Lemma SU_conservative_backward n (I: ordsysuni X n): 1 <= n -> SU X (SU_conservative I) -> SOU X n I.
proof: Proof. intros Leq (Delta & sigma & T & H). edestruct unification_downcast_eqs as (Sigma & tau & H1); eauto using equiv_pointwise_eqs, @H₀'. exists Sigma, tau; intuition idtac. eauto using equiv_eqs_pointwise. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)