proposition: Lemma Goldfarb_sharp (C: Const) (re: retract gonly C): ctype C (I None) = alpha → alpha → alpha -> OU 2 gonly ⪯ OU 2 C.
proof: Proof. intros. eapply unification_constants_monotone; eauto. intros [[]|]; cbn; eauto. 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)