En el ejercicio 3 parte a se pide resolver la siguiente derivación:
Examinando la solución propuesta, hay una regla de eliminación del Existe que me genera dudas:
En la slide del teórico, página 6, dice que esta regla se puede aplicar si y no está libre en Bottom y en las hipótesis para probar Bottom.
Sin embargo y si ocurre libre en las hipótesis eliminadas por la regla 2. Estoy confundido o esa restricción sobre las ocurrencias libres de y solo aplica para las premisas y no para las hipótesis generadas?
Muchas gracias, saludos!