∀ {α : Type u} {β : α → Type v} (entries : Multiset (Sigma β)) (nodupKeys : entries.NodupKeys)
  (entries_1 : Multiset (Sigma β)) (nodupKeys_1 : entries_1.NodupKeys),
  ({ entries := entries, nodupKeys := nodupKeys } = { entries := entries_1, nodupKeys := nodupKeys_1 }) =
    (entries = entries_1)