∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  [inst_3 : (k : α) → BEq (β k)] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    Std.DHashMap.Internal.Raw.WFImp ↑m₂ →
      m₁.beq m₂ =
        Std.Internal.List.beqModel (Std.DHashMap.Internal.toListModel (↑m₁).buckets)
          (Std.DHashMap.Internal.toListModel (↑m₂).buckets)