(motive : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u_1) →
  (x : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) →
    ((e : Lean.Expr) →
        (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
          motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core e lhs rhs)) →
      ((e : Lean.Expr) →
          (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
            motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore e lhs rhs)) →
        ((e : Lean.Expr) →
            (natStructId : ℕ) →
              (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat e natStructId lhs rhs)) →
          ((e : Lean.Expr) →
              (natStructId : ℕ) →
                (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                  motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat e natStructId lhs rhs)) →
            ((c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) →
                (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                  motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring c lhs)) →
              ((c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) →
                  (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                    motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq c lhs)) →
                (Unit → motive Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.oneGtZero) →
                  ((a b : Lean.Expr) →
                      (la lb : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                        motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEq a b la lb)) →
                    ((a b : Lean.Expr) →
                        (natStructId : ℕ) →
                          (la lb : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                            motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat a b natStructId la lb)) →
                      ((c₁ c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
                          motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine c₁ c₂)) →
                        ((c₁ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
                            (k : ℕ) → motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm c₁ k)) →
                          ((h : Lean.FVarId) → motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.dec h)) →
                            ((c₁ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) →
                                (decVar : Lean.FVarId) →
                                  (h : Lean.Meta.Grind.Arith.Linear.UnsatProof) →
                                    (decVars : Array Lean.FVarId) →
                                      motive
                                        (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit c₁ decVar h
                                          decVars)) →
                              ((x : Lean.Grind.Linarith.Var) →
                                  (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) →
                                    (c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
                                      motive (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst x c₁ c₂)) →
                                motive x