∀ (motive : Lean.Grind.CommRing.Poly → Sort u_1) (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)),
  (match Lean.Grind.CommRing.Poly.num 0 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_1 ()