 Again, pretending for the moment that every element of the domain has a name, the soundness of these rules is evident. (An instructive exercise, given the negation rules for classical logic, is to show that the rules for \(\exists\) (for \(\forall\)) are derivable from the rules for \(\forall\) (for \(\exists\)) and the definition of \(\exists x(A(x))\) as \(\neg\forall x\neg(A(x))\) (the definition of \(\forall x(A(x))\) as \(\neg\exists x\neg(A(x))\)). The restriction that the special term of the subproof not occur in the conclusion of \(\exists\)-Elimination turns out to correspond exactly to the restriction on reiteration into general subproofs.)