Existential quantification of a n-ary relation over its arguments to build a dependent pair (eg. Sigma type).
Given a (type of) relation `p : [t_1, t_2 ... t_n] x r` where `t_i` and `r` are types, `Ex` builds the type `Σ (x_1 : t_1). Σ (x_2 : t_2) ... . r` For example: ``` λ> Ex [Nat,Nat] LTE (x : Nat ** (x : Nat ** LTE x x)) ``` Which is the type of a pair of natural numbers along with a proof that the first is smaller or equal than the second.