∀ {γ : Type} (newEntries : List Lean.KeyedDeclsAttribute.OLeanEntry) (table : Lean.KeyedDeclsAttribute.Table γ)
  (declNames erased : Lean.PHashSet Lean.Name) (newEntries_1 : List Lean.KeyedDeclsAttribute.OLeanEntry)
  (table_1 : Lean.KeyedDeclsAttribute.Table γ) (declNames_1 erased_1 : Lean.PHashSet Lean.Name),
  ({ newEntries := newEntries, table := table, declNames := declNames, erased := erased } =
      { newEntries := newEntries_1, table := table_1, declNames := declNames_1, erased := erased_1 }) =
    (newEntries = newEntries_1 ∧ table = table_1 ∧ declNames = declNames_1 ∧ erased = erased_1)