{motive : Lean.Meta.Grind.Arith.Linear.ProofM.State → Sort u} →
  ((cache : Std.HashMap UInt64 Lean.Expr) →
      (varDecls : Std.HashMap Lean.Grind.Linarith.Var Lean.Expr) →
        (polyDecls : Std.HashMap Lean.Grind.Linarith.Poly Lean.Expr) →
          (exprDecls : Std.HashMap Lean.Meta.Grind.Arith.Linear.LinExpr Lean.Expr) →
            (ringPolyDecls : Std.HashMap Lean.Grind.CommRing.Poly Lean.Expr) →
              (ringExprDecls : Std.HashMap Lean.Meta.Grind.Arith.CommRing.RingExpr Lean.Expr) →
                (ringVarDecls : Std.HashMap Lean.Grind.Linarith.Var Lean.Expr) →
                  motive
                    { cache := cache, varDecls := varDecls, polyDecls := polyDecls, exprDecls := exprDecls,
                      ringPolyDecls := ringPolyDecls, ringExprDecls := ringExprDecls, ringVarDecls := ringVarDecls }) →
    (t : Lean.Meta.Grind.Arith.Linear.ProofM.State) → motive t