∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited β] {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α},
      Std.DHashMap.Internal.Raw₀.Const.get! m a =
        Std.Internal.List.getValue! a (Std.DHashMap.Internal.toListModel (↑m).buckets)