proposition: Lemma Goldfarb_remove: H10 ⪯ OU 2 ag /\ OU 2 ag ⪯ OU 2 gonly.
proof: Proof. split. eapply Goldfarb. eapply (@remove_constants_reduction ag gonly); eauto. intros [[]|]; cbn; eauto. intros [[[]|]|]; cbn; eauto. destruct eq_dec; intuition discriminate. 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)