∀ {α β σ : Type} {toPersistentEnvExtensionDescrCore : Lean.PersistentEnvExtensionDescrCore α β σ}
  {exportEntriesFn : σ → Array α} {toPersistentEnvExtensionDescrCore_1 : Lean.PersistentEnvExtensionDescrCore α β σ}
  {exportEntriesFn_1 : σ → Array α},
  { toPersistentEnvExtensionDescrCore := toPersistentEnvExtensionDescrCore, exportEntriesFn := exportEntriesFn } =
      { toPersistentEnvExtensionDescrCore := toPersistentEnvExtensionDescrCore_1,
        exportEntriesFn := exportEntriesFn_1 } →
    toPersistentEnvExtensionDescrCore = toPersistentEnvExtensionDescrCore_1 ∧ exportEntriesFn = exportEntriesFn_1