∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [LawfulBEq α]
  {p : α → β → Bool}, m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p a (Std.DHashMap.Const.get m a h) = false