{motive : Lean.Meta.Grind.Context → Sort u} →
  (t : Lean.Meta.Grind.Context) →
    ((simp : Lean.Meta.Simp.Context) →
        (simpMethods : Lean.Meta.Simp.Methods) →
          (config : Lean.Grind.Config) →
            (anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef)) →
              (cheapCases reportMVarIssue : Bool) →
                (splitSource : Lean.Meta.Grind.SplitSource) →
                  (symPrios : Lean.Meta.Grind.SymbolPriorities) →
                    (extensions : Lean.Meta.Grind.ExtensionStateArray) →
                      (debug : Bool) →
                        motive
                          { simp := simp, simpMethods := simpMethods, config := config, anchorRefs? := anchorRefs?,
                            cheapCases := cheapCases, reportMVarIssue := reportMVarIssue, splitSource := splitSource,
                            symPrios := symPrios, extensions := extensions, debug := debug }) →
      motive t