∀ {α : Type u} [inst : Lean.Grind.Semiring α] (h : Equivalence (Lean.Grind.Ring.OfSemiring.r α))
  (q₁ q₂ : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.rel✝ h q₁ q₂ = q₁.liftOn₂ q₂ (fun a₁ a₂ => Lean.Grind.Ring.OfSemiring.r α a₁ a₂) ⋯