proposition: Lemma SU_U: SU ⪯ U X.
proof: Proof. exists (sysuni_uni). intros I; split; intros (Delta & sigma & H1 & H2); exists Delta; exists sigma; destruct I; intuition idtac; cbn [sᵤ tᵤ sysuni_uni] 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 Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)