Práctico 8

Hola:

En la derivación de la derecha, la clave está en encontrar la sustitución apropiada para la eliminación del para todo con la hipótesis $\forall y (x =' y \to \varphi[y/x])$.

Aquí te recomiendo que busques un término $t$ para sustituir la $y$ de manera que te quede algo así:

• $x ='t \to \varphi[t/x]$

donde:

• $x =' t$ se pueda derivar sin hipótesis
• $\varphi[t/x]$ sea igual $\varphi$

Con eso sale fácil.