∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (x x_1 : Lean.Grind.CommRing.Poly)
  (h_1 : (a b : ℤ) → motive (Lean.Grind.CommRing.Poly.num a) (Lean.Grind.CommRing.Poly.num b))
  (h_2 :
    (a : ℤ) →
      (a_1 : Lean.Grind.CommRing.Mon) →
        (a_2 : Lean.Grind.CommRing.Poly) →
          (b : ℤ) →
            (b_1 : Lean.Grind.CommRing.Mon) →
              (b_2 : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add a a_1 a_2) (Lean.Grind.CommRing.Poly.add b b_1 b_2))
  (h_3 : (x x_2 : Lean.Grind.CommRing.Poly) → motive x x_2),
  (∀ (a b : ℤ), x = Lean.Grind.CommRing.Poly.num a → x_1 = Lean.Grind.CommRing.Poly.num b → False) →
    (∀ (a : ℤ) (a_1 : Lean.Grind.CommRing.Mon) (a_2 : Lean.Grind.CommRing.Poly) (b : ℤ) (b_1 : Lean.Grind.CommRing.Mon)
        (b_2 : Lean.Grind.CommRing.Poly),
        x = Lean.Grind.CommRing.Poly.add a a_1 a_2 → x_1 = Lean.Grind.CommRing.Poly.add b b_1 b_2 → False) →
      (match x, x_1 with
        | Lean.Grind.CommRing.Poly.num a, Lean.Grind.CommRing.Poly.num b => h_1 a b
        | Lean.Grind.CommRing.Poly.add a a_1 a_2, Lean.Grind.CommRing.Poly.add b b_1 b_2 => h_2 a a_1 a_2 b b_1 b_2
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1