proposition: Lemma Goldfarb': H10 ⪯ SOU ag 2.
proof: Proof. exists H10_to_SOU; intros x; split. - eapply H10_SU. - eapply SU_H10. Qed.
imports: RelationClasses Morphisms Init.Wf List Lia Init.Nat Setoid Undecidability.HOU(calculus.calculus unification.unification)