En el video de openfing del practico 8 en el minuto 2:07:40 se dice que se puede remplazar una parte de la derivación con otra ya vista y que utiliza otras hipótesis para no generar problemas con la regla de introducción del para todo. Sin embargo, esta forma deja sin utilizar la hipótesis 5 generada mas abajo. La cual si se incluye en las restricciones de la introducción del para todo genera problemas al no poder garantizar que x no sea libre para phi.
¿Las hipótesis no utilizadas tambien cuentan para la verificación de las restricciones de la introducción del para todo?