proposition: Lemma U_SU: U X ⪯ SU.
proof: Proof. exists (uni_sysuni); intros I. split; intros (Delta & sigma & H1 & H2); exists Delta; exists sigma; intuition idtac. firstorder idtac; injection H; intros; subst; trivial. eapply H2; firstorder. Qed.
imports: List Lia Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification)