{motive_1 : Lean.Meta.Grind.Arith.Linear.RingEqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof → Sort u} →
    ((p : Lean.Grind.CommRing.Poly) →
        (h : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) → motive_2 h → motive_1 { p := p, h := h }) →
      ((a b : Lean.Expr) →
          (ra rb : Lean.Grind.CommRing.Expr) →
            motive_2 (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core a b ra rb)) →
        ((c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) →
            motive_1 c → motive_2 (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm c)) →
          ((c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) →
              (val : ℤ) →
                (x n : Lean.Grind.Linarith.Var) →
                  motive_1 c → motive_2 (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.cancelDen c val x n)) →
            (t : Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof) → motive_2 t