Resposta

Vamos ver se eu consigo escrever isso sem utilizar caracteres especiais:

Lema: D => G == ~D v G

(existe x.D) => G == ~(existe x.D) v G == (paratodo x.~D) v G == paratodo x.(~D v G) ** == paratodo x.(D => G).

** isso pode ser feito porque X não é variável livre em G.