proposition: Lemma OU_SOU n: OU n X ⪯ SOU n.
proof: Proof. exists (orduni_ordsysuni n); intros I. split; intros (Delta & sigma & H1 & H2); exists Delta; exists sigma; intuition idtac. firstorder idtac; injection H; intros; subst; trivial. firstorder. Qed.
imports: List Lia Morphisms Undecidability.HOU(std.std calculus.calculus unification.higher_order_unification unification.systemunification)