7.2.5 Eliminación del universal

Otra fácil de entender:

$$\begin{fitch*} \par n & \forall x A \\ \par \hline \par & A\{t/x\} & E$\forall$\ n,t \par \end{fitch*}$$

Si sabemos que $A$ se cumple para cualquier elemento, entonces podemos elegir un elemento cualquiera y sabemos que se cumple $A$ en ese elemento.