No puedo llegar a una solución...voy rumbeado?
Sí.
¿Cómo se prueba un existencial? Hay que dar el testigo.
Si observamos los similitudes entre las premisas y la conclusión, vemos que vamos a precisar la sustitución [g(x)/y].
![\infer[I_\exists]{(\exists y)(P(x,y) \land \lnot y =' f(x))}{P(x,g(x)) \land \lnot g(x) =' f(x)}](https://eva.fing.edu.uy/filter/tex/pix.php/bb3c05bb0b2d2c8370a8f36667681bcc.png "\infer[I_\exists]{(\exists y)(P(x,y) \land \lnot y =' f(x))}{P(x,g(x)) \land \lnot g(x) =' f(x)}")
.
Luego se puede usar una 
; una 
para el subárbol izquierdo con la hip. 1 y hay que usar la hipótesis que genera la 
de la hip. 2 para el subárbol derecho.
El tema es dónde meter la para que cumpla con las restricciones.
Tip (general): hacer las lo más abajo posible.
Acá lo podríamos usar para probar bottom.
Saludos