proposition: Lemma SOU_OU n (I: ordsysuni n) (H: ord' L₀' < n): SOU n I <-> OU n X (ordsysuni_orduni I H).
proof: Proof. split; intros (Delta & sigma & H1 & H2); exists Delta; exists sigma; intuition idtac; cbn [s₀ t₀ ordsysuni_orduni] in *. rewrite !linearize_terms_subst, linearize_terms_equiv. now apply equiv_pointwise_eqs. eapply equiv_eqs_pointwise; [|eassumption]. now rewrite <-linearize_terms_equiv, <-!linearize_terms_subst. Qed.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)