{motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
  (t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) →
    ((e : Lean.Expr) →
        (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
          motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.core e lhs rhs)) →
      ((e : Lean.Expr) →
          (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
            motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore e lhs rhs)) →
        ((c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr) →
            (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
              motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ring c lhs)) →
          ((e : Lean.Expr) →
              (natStructId : ℕ) →
                (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                  motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.coreOfNat e natStructId lhs rhs)) →
            ((e : Lean.Expr) →
                (natStructId : ℕ) →
                  (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                    motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat e natStructId lhs rhs)) →
              ((c₁ c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
                  motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine c₁ c₂)) →
                ((c₁ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
                    (k : ℕ) → motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.norm c₁ k)) →
                  ((h : Lean.FVarId) → motive_4 (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_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofDiseqSplit c₁ decVar h decVars)) →
                      motive_4 Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.oneGtZero →
                        ((a b : Lean.Expr) →
                            (la lb : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                              motive_4 (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_4
                                    (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ofEqOfNat a b natStructId la lb)) →
                            ((c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr) →
                                (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                                  motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.ringEq c lhs)) →
                              ((x : Lean.Grind.Linarith.Var) →
                                  (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) →
                                    (c₂ : Lean.Meta.Grind.Arith.Linear.IneqCnstr) →
                                      motive_4 (Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst x c₁ c₂)) →
                                motive_4 t