Update quantifiers_and_equality.md

quantifiers_and_equality.md

@@ -927,23 +927,25 @@ You should also try to understand why the reverse implication is not derivable i
 
 2. It is often possible to bring a component of a formula outside a
    universal quantifier, when it does not depend on the quantified
-   variable. Try proving these (one direction of the second of these
-   requires classical logic):
+   variable. Try proving these:
 
 ```lean
 variable (α : Type) (p q : α → Prop)
 variable (r : Prop)
 
 example : α → ((∀ x : α, r) ↔ r) := sorry
-example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry
 example : (∀ x, r → p x) ↔ (r → ∀ x, p x) := sorry
+
+open classical
+example : (∀ x, p x ∨ r) ↔ (∀ x, p x) ∨ r := sorry
 ```
 
 3. Consider the "barber paradox," that is, the claim that in a certain
    town there is a (male) barber that shaves all and only the men who
    do not shave themselves. Prove that this is a contradiction:
 
 ```lean
+open classical
 variable (men : Type) (barber : men)
 variable (shaves : men → men → Prop)