test_russell2

theorem test_russell2 {α : Type _} (S : α → Prop) : ¬ (∀ x : α, S x ↔ ¬ S x) := by sorry