∀ {config : Lean.Grind.Config} {extensions : Lean.Meta.Grind.ExtensionStateArray}
  {extra : Lean.PArray Lean.Meta.Grind.EMatchTheorem} {extraInj : Lean.PArray Lean.Meta.Grind.InjectiveTheorem}
  {extraFacts : Lean.PArray Lean.Expr} {symPrios : Lean.Meta.Grind.SymbolPriorities} {norm : Lean.Meta.Simp.Context}
  {normProcs : Array Lean.Meta.Simprocs} {anchorRefs? : Option (Array Lean.Meta.Grind.AnchorRef)}
  {config_1 : Lean.Grind.Config} {extensions_1 : Lean.Meta.Grind.ExtensionStateArray}
  {extra_1 : Lean.PArray Lean.Meta.Grind.EMatchTheorem} {extraInj_1 : Lean.PArray Lean.Meta.Grind.InjectiveTheorem}
  {extraFacts_1 : Lean.PArray Lean.Expr} {symPrios_1 : Lean.Meta.Grind.SymbolPriorities}
  {norm_1 : Lean.Meta.Simp.Context} {normProcs_1 : Array Lean.Meta.Simprocs}
  {anchorRefs?_1 : Option (Array Lean.Meta.Grind.AnchorRef)},
  { config := config, extensions := extensions, extra := extra, extraInj := extraInj, extraFacts := extraFacts,
        symPrios := symPrios, norm := norm, normProcs := normProcs, anchorRefs? := anchorRefs? } =
      { config := config_1, extensions := extensions_1, extra := extra_1, extraInj := extraInj_1,
        extraFacts := extraFacts_1, symPrios := symPrios_1, norm := norm_1, normProcs := normProcs_1,
        anchorRefs? := anchorRefs?_1 } →
    config = config_1 ∧
      extensions = extensions_1 ∧
        extra = extra_1 ∧
          extraInj = extraInj_1 ∧
            extraFacts = extraFacts_1 ∧
              symPrios = symPrios_1 ∧ norm = norm_1 ∧ normProcs = normProcs_1 ∧ anchorRefs? = anchorRefs?_1