{motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
  (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) →
    ((a b : Lean.Expr) →
        (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
          motive_6 (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.core a b lhs rhs)) →
      ((c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) →
          (lhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
            motive_6 (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.ring c lhs)) →
        ((a b : Lean.Expr) →
            (natStructId : ℕ) →
              (lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr) →
                motive_6 (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.coreOfNat a b natStructId lhs rhs)) →
          ((c : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) →
              motive_6 (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.neg c)) →
            ((k₁ k₂ : ℤ) →
                (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) →
                  (c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) →
                    motive_6 (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst k₁ k₂ c₁ c₂)) →
              ((k : ℤ) →
                  (c₁ : Lean.Meta.Grind.Arith.Linear.EqCnstr) →
                    (c₂ : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) →
                      motive_6 (Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.subst1 k c₁ c₂)) →
                motive_6 Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.oneNeZero → motive_6 t