∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β},
      (Std.DHashMap.Raw.Const.toList ↑(m.insert k v)).Perm
        ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) (Std.DHashMap.Raw.Const.toList ↑m))