Hola.
Teniendo en cuenta la precedencia de los cuantificadores en lógica de predicados es correcto poner el paréntesis al traducir a Coq tal cual lo indicás.
Este ejercicio no está formalizado en la plantilla; la escritura por parte de uds estaba pensada para que vieran estas cosas.
Saludos, Carlos