{motive : Lean.Meta.Grind.State → Sort u} →
  ((congrThms : Lean.PHashMap Lean.Meta.Grind.CongrTheoremCacheKey Lean.Meta.CongrTheorem) →
      (simp : Lean.Meta.Simp.State) →
        (lastTag : Lean.Name) →
          (issues : List Lean.MessageData) →
            (counters : Lean.Meta.Grind.Counters) →
              (splitDiags : Lean.PArray Lean.Meta.Grind.SplitDiagInfo) →
                (lawfulEqCmpMap reflCmpMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)) →
                  (anchors : Lean.PHashMap Lean.Meta.Sym.ExprPtr UInt64) →
                    motive
                      { congrThms := congrThms, simp := simp, lastTag := lastTag, issues := issues,
                        counters := counters, splitDiags := splitDiags, lawfulEqCmpMap := lawfulEqCmpMap,
                        reflCmpMap := reflCmpMap, anchors := anchors }) →
    (t : Lean.Meta.Grind.State) → motive t