[Agda] \exists definition

[Serge D. Mechveliani]

Please, 
where is the definition for the  \exists  math symbol (type constructor?) ?
This is on  Agda-2.3.0.1 + Standard library lib-0.6.

module Data.Nat.GCD  contains (in the end) a declaration 

       gcd : (m n : Nat) -> \exists \lambda d -> GCD m n d

(I replace math symbols here).
I do not find  \exists  in the key words in Reference manual.
And so far, do not find its definition in the  lib-0.6  sources.
To use `grep' in Linux, I need to enter this symbol to the command line 
of `grep', and this occurs difficult.

Thanks,

------
Sergei