(motive : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof → Sort u_1) →
  (x : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof) →
    ((a b : Lean.Expr) →
        (lhs rhs : Lean.Grind.CommRing.Expr) →
          motive (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core a b lhs rhs)) →
      ((c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) →
          (val : ℤ) →
            (x n : Lean.Grind.Linarith.Var) →
              motive (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen c val x n)) →
        motive x