{P : Sort u} →
  {newEntries : List Lean.AttributeExtensionOLeanEntry} →
    {map : Std.HashMap Lean.Name Lean.AttributeImpl} →
      {newEntries' : List Lean.AttributeExtensionOLeanEntry} →
        {map' : Std.HashMap Lean.Name Lean.AttributeImpl} →
          { newEntries := newEntries, map := map } = { newEntries := newEntries', map := map' } →
            (newEntries = newEntries' → map = map' → P) → P