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.