Fuente TeX:

(\forall x) (P(x,g(z,y)) \rightarrow ((\forall y) Q(y,y))[g(z,y)/y] )