∀ {α β σ : Type} (name : autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam) (mkInitial : IO σ)
  (ofOLeanEntry : σ → α → Lean.ImportM β) (toOLeanEntry : β → α) (addEntry : σ → β → σ) (finalizeImport : σ → σ)
  (exportEntry? : Lean.OLeanLevel → α → Option α)
  (name_1 : autoParam Lean.Name Lean.ScopedEnvExtension.Descr.name._autoParam) (mkInitial_1 : IO σ)
  (ofOLeanEntry_1 : σ → α → Lean.ImportM β) (toOLeanEntry_1 : β → α) (addEntry_1 : σ → β → σ) (finalizeImport_1 : σ → σ)
  (exportEntry?_1 : Lean.OLeanLevel → α → Option α),
  ({ name := name, mkInitial := mkInitial, ofOLeanEntry := ofOLeanEntry, toOLeanEntry := toOLeanEntry,
        addEntry := addEntry, finalizeImport := finalizeImport, exportEntry? := exportEntry? } =
      { name := name_1, mkInitial := mkInitial_1, ofOLeanEntry := ofOLeanEntry_1, toOLeanEntry := toOLeanEntry_1,
        addEntry := addEntry_1, finalizeImport := finalizeImport_1, exportEntry? := exportEntry?_1 }) =
    (name = name_1 ∧
      mkInitial = mkInitial_1 ∧
        ofOLeanEntry = ofOLeanEntry_1 ∧
          toOLeanEntry = toOLeanEntry_1 ∧
            addEntry = addEntry_1 ∧ finalizeImport = finalizeImport_1 ∧ exportEntry? = exportEntry?_1)