∀ {α : Type}
  (toPersistentEnvExtension toPersistentEnvExtension_1 :
    Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)),
  ({ toPersistentEnvExtension := toPersistentEnvExtension } =
      { toPersistentEnvExtension := toPersistentEnvExtension_1 }) =
    (toPersistentEnvExtension = toPersistentEnvExtension_1)