Solution
= Solution
The result of part (ii), with $R$ replaced by $\neg R$, first yields $\forall y\neg\neg R(y)$. To show every use of the derived rule explicitly, one can instead write:
``
1. ¬∃x ¬R(x) premise
2. ¬R(a) assumption [i], a fresh
3. ∃x ¬R(x) ∃I, 2
4. ⊥ ¬E, 1, 3
5. ¬¬R(a) ¬I, 2–4, discharging [i]
6. R(a) ¬¬E, 5
7. ∀y R(y) ∀I, 6
``
The classical step is <double-negation elimination> at line 6. Freshness at line 7 holds after discharging the temporary assumption.