∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] (f f_1 : α → Bool),
  f = f_1 → ∀ (m m_1 : Std.ExtHashSet α), m = m_1 → Std.ExtHashSet.filter f m = Std.ExtHashSet.filter f_1 m_1