[Agda] binder for existential quantifier

[Martin Escardo]

Dear Agda list members,

If I define the existential quantifier as follows:

   Ω = Set -- type of propositions

   data ∃ {X : Set} (A : X → Ω) : Ω where
     ∃-intro : (x₀ : X) → A x₀ → ∃(\(x : X) → A x)

then I have to write

   ∃(\(x : X) → A x)       (*)

rather than

   ∃ (x : X) → A x         (**)

as one can do with the universal quantifier.

This is tolerable, but I would prefer to be able to write (**).

Can this be done with a "syntax" declaration?

Thanks,
Martin