proposition: Lemma SU_monotone_backward n (I: ordsysuni X n): 1 <= n -> SOU X (S n) (SU_monotone I) -> SOU X n I.
proof: Proof. intros Leq (Delta & sigma & T & H). unfold OU. edestruct unification_downcast_eqs as (Sigma & tau & H1); eauto using equiv_pointwise_eqs, @H₀'. intros ???; eapply ordertyping_soundness; eauto. 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)