Uncurrying and Polymorphism
The other answers are good, I just wanted to make it explicit that currying for dependent types is
$$
\textstyle
\prod (x : A) . \prod (y : B(x)) . C(x, y)
\ \cong \ 
\prod (p : \sum (x : A) . B(x)) . C(\pi_1(p), \pi_2(p))
$$
which is more suggestive in Agda-style notation:
$$
(x : A) \to (y : B(x)) \to C(x,y)
\ \cong\ 
(p : (x : A) \times B(x)) \to C(\pi_1(p), \pi_2(p))
$$
In your case, replace $\Pi$ and $\Sigma$ with $\forall$ and $\exists$.