∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (p : Lean.Grind.CommRing.Poly)
  (h_1 : Unit → motive (Lean.Grind.CommRing.Poly.num 0)) (h_2 : (k : ℤ) → motive (Lean.Grind.CommRing.Poly.num k))
  (h_3 :
    (k : ℤ) →
      (m : Lean.Grind.CommRing.Mon) → (p : Lean.Grind.CommRing.Poly) → motive (Lean.Grind.CommRing.Poly.add k m p))
  (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p_1 : Lean.Grind.CommRing.Poly),
  p = Lean.Grind.CommRing.Poly.add k m p_1 →
    (match p with
      | Lean.Grind.CommRing.Poly.num 0 => h_1 ()
      | Lean.Grind.CommRing.Poly.num k => h_2 k
      | Lean.Grind.CommRing.Poly.add k m p => h_3 k m p) ≍
      h_3 k m p_1