∀ (p₂ : Lean.Grind.CommRing.Poly) (c : ℕ)
  (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ),
      motive (Lean.Grind.CommRing.Poly.num k) acc (acc.combineC (Lean.Grind.CommRing.Poly.mulConstC k p₂ c) c)) →
    (∀ (acc : Lean.Grind.CommRing.Poly) (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
        motive p (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c)
            (Lean.Grind.CommRing.Poly.mulC.go p₂ c p (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c)) →
          motive (Lean.Grind.CommRing.Poly.add k m p) acc
            (Lean.Grind.CommRing.Poly.mulC.go p₂ c p (acc.combineC (Lean.Grind.CommRing.Poly.mulMonC k m p₂ c) c))) →
      ∀ (p₁ acc : Lean.Grind.CommRing.Poly), motive p₁ acc (Lean.Grind.CommRing.Poly.mulC.go p₂ c p₁ acc)