{motive : Lean.Meta.Grind.Arith.Linear.NatStruct → Sort u} →
  (t : Lean.Meta.Grind.Arith.Linear.NatStruct) →
    ((id structId : ℕ) →
        (type : Lean.Expr) →
          (u : Lean.Level) →
            (natModuleInst : Lean.Expr) →
              (leInst? ltInst? lawfulOrderLTInst? isPreorderInst? orderedAddInst? isLinearInst? addRightCancelInst? :
                  Option Lean.Expr) →
                (rfl_q zero toQFn addFn smulFn : Lean.Expr) →
                  (termMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Lean.Expr × Lean.Expr)) →
                    motive
                      { id := id, structId := structId, type := type, u := u, natModuleInst := natModuleInst,
                        leInst? := leInst?, ltInst? := ltInst?, lawfulOrderLTInst? := lawfulOrderLTInst?,
                        isPreorderInst? := isPreorderInst?, orderedAddInst? := orderedAddInst?,
                        isLinearInst? := isLinearInst?, addRightCancelInst? := addRightCancelInst?, rfl_q := rfl_q,
                        zero := zero, toQFn := toQFn, addFn := addFn, smulFn := smulFn, termMap := termMap }) →
      motive t