[Agda] Binding two identifiers using user-defined syntax

[Jean-Philippe Bernardy]

>    syntax ∃₂ (λ x y → e) = ∃₂[ x y ] e

At the moment you need to have a constructor part between each "hole".
E.g. this would work:

syntax ∃₂ (λ x y → e) = ∃₂[ x , y ] e

Cheers,
JP.