Hola, tengo una duda hacerca de la 2da derivación (link examen :http://dl.dropboxusercontent.com/u/58373398/L%C3%B3gica/Ex%C3%A1menes/log-ex-2005-jul.pdf )
En ella cuando quiere probar ¬P(x) v Q(w) utiliza una eliminacion del para todo, obteniendo asi: ∀y(¬P(x) v Q(y)).
Mi duda es como realizó la sustitución de Q(w) por Q(y) ya que la regla de derivación permitiria una sustitución de la forma [t/y] no [t/w].
![\infer[E \forall]{\neg P(X) \lor Q(w)}{\forall y (\neg P(X) \lor Q(Y))}](https://eva.fing.edu.uy/filter/tex/pix.php/eef564c6cfa61ff9d0ffecb22660f85e.png "\infer[E \forall]{\neg P(X) \lor Q(w)}{\forall y (\neg P(X) \lor Q(Y))}")
