proposition: Lemma unification_conservative_backward n (I: orduni n X): 1 <= n -> U X (unification_conservative I) -> OU n X I.
proof: Proof. intros Leq (Delta & sigma & T & H). unfold OU. eapply unification_downcast; eauto. Qed.
imports: PeanoNat Lia List Undecidability.HOU(calculus.calculus concon.conservativity_constants unification.higher_order_unification unification.systemunification unification.nth_order_unification)