Hola, buenas. Haciendo el ejercicio en cuestión, llegue a esta expresión que aparece acá abajo (luego verifiqué en el video del práctico y llegan a la misma, de hecho, esta screenshot es justamente de dicho video). El tema es que al momento de hacerlo, pensé que no era una sustitución válida puesto que entiendo que introduce una ligadura donde antes no la habia:
Originalmente, en el miembro derecho del or, teníamos un existe cuantificando una igualdad, pero las variables de dicha igualdad son libres respecto al existe. Luego de la sustitución, nos queda que esa misma igualdad ahora tiene un término que esta ligado al cuantificador. 
Tenía entendido (del teórico) que esta situación es problemática, que generalmente se busca no introducir nuevas ligaduras despues de realizar una sustitución. Sin embargo, en el video del práctico no se menciona en lo absoluto que en este ejemplo en particular esto sea un problema, entonces no entiendo, ¿esta sustitución es válida? ¿estoy equivocado en pensar que introduce una nueva ligadura?
Muchas gracias de antemano!