{P : Sort u} →
  {p : Lean.Grind.CommRing.Poly} →
    {k₁ : ℤ} →
      {d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation} →
        {k₂ : ℤ} →
          {m₂ : Lean.Grind.CommRing.Mon} →
            {c : Lean.Meta.Grind.Arith.CommRing.EqCnstr} →
              {p' : Lean.Grind.CommRing.Poly} →
                {k₁' : ℤ} →
                  {d' : Lean.Meta.Grind.Arith.CommRing.PolyDerivation} →
                    {k₂' : ℤ} →
                      {m₂' : Lean.Grind.CommRing.Mon} →
                        {c' : Lean.Meta.Grind.Arith.CommRing.EqCnstr} →
                          Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p k₁ d k₂ m₂ c =
                              Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p' k₁' d' k₂' m₂' c' →
                            (p = p' → k₁ = k₁' → d = d' → k₂ = k₂' → m₂ = m₂' → c = c' → P) → P