{α β σ : Type} →
  {P : Sort u} →
    {toEnvExtension : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)} →
      {name : Lean.Name} →
        {addImportedFn : Array (Array α) → Lean.ImportM σ} →
          {addEntryFn : σ → β → σ} →
            {exportEntriesFn : Lean.Environment → σ → Lean.OLeanLevel → Array α} →
              {statsFn : σ → Std.Format} →
                {toEnvExtension' : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)} →
                  {name' : Lean.Name} →
                    {addImportedFn' : Array (Array α) → Lean.ImportM σ} →
                      {addEntryFn' : σ → β → σ} →
                        {exportEntriesFn' : Lean.Environment → σ → Lean.OLeanLevel → Array α} →
                          {statsFn' : σ → Std.Format} →
                            { toEnvExtension := toEnvExtension, name := name, addImportedFn := addImportedFn,
                                  addEntryFn := addEntryFn, exportEntriesFn := exportEntriesFn, statsFn := statsFn } =
                                { toEnvExtension := toEnvExtension', name := name', addImportedFn := addImportedFn',
                                  addEntryFn := addEntryFn', exportEntriesFn := exportEntriesFn',
                                  statsFn := statsFn' } →
                              (toEnvExtension ≍ toEnvExtension' →
                                  name = name' →
                                    addImportedFn ≍ addImportedFn' →
                                      addEntryFn ≍ addEntryFn' →
                                        exportEntriesFn ≍ exportEntriesFn' → statsFn ≍ statsFn' → P) →
                                P