∀ {α σ : Type} (name : autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam)
  (addEntryFn : σ → α → σ) (addImportedFn : Array (Array α) → σ) (toArrayFn : List α → Array α)
  (exportEntriesFnEx? : Option (Lean.Environment → σ → List α → Lean.OLeanLevel → Array α))
  (asyncMode : Lean.EnvExtension.AsyncMode) (replay? : Option (List α → σ → σ → List α × σ))
  (name_1 : autoParam Lean.Name Lean.SimplePersistentEnvExtensionDescr.name._autoParam) (addEntryFn_1 : σ → α → σ)
  (addImportedFn_1 : Array (Array α) → σ) (toArrayFn_1 : List α → Array α)
  (exportEntriesFnEx?_1 : Option (Lean.Environment → σ → List α → Lean.OLeanLevel → Array α))
  (asyncMode_1 : Lean.EnvExtension.AsyncMode) (replay?_1 : Option (List α → σ → σ → List α × σ)),
  ({ name := name, addEntryFn := addEntryFn, addImportedFn := addImportedFn, toArrayFn := toArrayFn,
        exportEntriesFnEx? := exportEntriesFnEx?, asyncMode := asyncMode, replay? := replay? } =
      { name := name_1, addEntryFn := addEntryFn_1, addImportedFn := addImportedFn_1, toArrayFn := toArrayFn_1,
        exportEntriesFnEx? := exportEntriesFnEx?_1, asyncMode := asyncMode_1, replay? := replay?_1 }) =
    (name = name_1 ∧
      addEntryFn = addEntryFn_1 ∧
        addImportedFn = addImportedFn_1 ∧
          toArrayFn = toArrayFn_1 ∧
            exportEntriesFnEx? = exportEntriesFnEx?_1 ∧ asyncMode = asyncMode_1 ∧ replay? = replay?_1)