∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {f : α → Bool}, Std.ExtHashSet.filter f m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.get k h) = false