∀ {α : Type u_1} {x : BEq α} {x_1 : Hashable α} {β : Type u_2} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m : Std.ExtDHashMap α fun x => β),
  ∀ a ∈ m, ∀ (m_1 : Std.DHashMap α fun x => β), m = Std.ExtDHashMap.mk m_1 → a ∈ Std.ExtDHashMap.mk m_1