proposition: Lemma Goldfarb_Huet X: OU 2 gonly ⪯ OU 3 gonly /\ OU 3 gonly ⪯ OU 3 cfree /\ OU 3 cfree ⪯ OU 3 X.
proof: Proof. repeat split. eapply unification_step; eauto. eapply remove_constants_reduction; eauto. intros []. intros [[]|]; cbn; eauto. eapply unification_constants_monotone; eauto. intros []. Qed.
imports: List Arith Lia Morphisms Setoid Undecidability.HOU(calculus.calculus) Undecidability.HOU(unification.higher_order_unification unification.nth_order_unification concon.conservativity_constants concon.conservativity concon.constants) Undecidability.HOU(second_order.diophantine_equations second_order.goldfarb.reduction)