Is it possible to prove that the encoding of existentials in System F is valid? In Girard's Proofs and Types, under item 11.3.5, second-order existential quantification is encoded in System F using universal quantification as follows:
$$
\Sigma X.V \equiv \Pi Y. (\Pi X.(V \to Y)) \to Y
$$
Is it possible to prove this encoding is correct using natural deduction or sequent calculus? In other words, is it possible to prove the following in System F extended with existentials?
$$
(1)\quad \Sigma X.V \vdash \Pi Y. (\Pi X.(V \to Y)) \to Y
\\
(2)\quad \Pi Y. (\Pi X.(V \to Y)) \to Y \vdash \Sigma X.V
$$
I think I can prove (1), but not (2).
In case these propositions are invalid, how can we be sure the encoding is correct?
Thank you.
PS.
I understand intuitively why the encoding makes sense, but would like to understand the formal reasons. 
This encoding is widespread, but I can't find a proof of its validity. In Haskell, for example, it is used to simulate existential types and in similar questions such as this one the explanation is informal. In this self-answered question, which attempts to produce a proof, I think there are errors involving invalid variable capturing.
Edit: Proof attempt of (2) based on Andrej's answer
I.
$$
{
\Pi Y. (\Pi X.(VX \to Y)) \to Y
\over
(\Pi X.(VX \to (\Sigma Z. V Z))) \to (\Sigma Z. V Z)
} \, \Pi E 
$$
II.
$$
{
\hspace{8em}
\over
VT
} u
\\
{
\hspace{8em}
\over
\Sigma Z. VZ
} \Sigma I
\\
{
\hspace{10em}
\over
V T \to (\Sigma Z. VZ)
} \to I_u
\\
{
\hspace{10em}
\over
\Pi X. (V X \to (\Sigma Z. VZ))
} \Pi I_T
$$
III. From I and II:
$$
{
\quad
(\Pi X. (V X \to (\Sigma Z. V Z))) \to (\Sigma Z. V Z)
\qquad
\Pi X. (V X \to (\Sigma Z. V Z))
\quad
\over
\Sigma Z. VZ
} \to E
$$
 A: For second-order logic with Natural Deduction, you can see :

  
*
  
*Dag Prawitz, Natural Deduction A Proof-Theoretical Study (1965)
  

or :

  
*
  
*Dirk van Dalen, Logic and Structure (5th ed - 2013).
  

Both prove :

$ΣX.V \equiv ΠY.(ΠX.(V→Y))→Y$.

See van Dalen, page 150, Theorem 5.5 (e) :


$\vdash_2 ∃X^n \varphi ↔ ∀X^0(∀X^n((\varphi → X^0) → X^0)$.


Proof
$${ [∀X^n(\varphi→X)] \over (\varphi→X) } \, (\forall^2E)$$
$${ [\varphi] \quad (\varphi→X) \over X } \, (\rightarrow E)$$
$${ ∀X^n(\varphi→X)→X \over (\varphi→X) } \, (\rightarrow I) \, \text{(discharging the 1st assumption)}$$
$${ \exists X^n \varphi \quad ∀X^n(\varphi→X)→X \over ∀X^n(\varphi→X)→X } \, (\exists^2E) \, \text{(discharging the 2nd assumption)}$$
$${ ∀X^n(\varphi→X)→X \over \forall X(∀X^n(\varphi→X)→X) } \, (\forall^2I) $$
Thus :


$\vdash_2 ∃X^n \varphi \rightarrow ∀X^0(∀X^n(\varphi \rightarrow X^0) \rightarrow X^0)$.



For the other direction :
$${ [\varphi] \over \exists X^n \varphi } \, (\exists^2I)$$
$${ \varphi \rightarrow \exists X^n \varphi \over \forall X^n (\varphi \rightarrow \exists X^n \varphi) } \, (\forall^2I)$$
In parallel :
$${∀X^0(∀X^n(\varphi \rightarrow X^0) \rightarrow X^0) \over ∀X^n(\varphi \rightarrow \exists X^n \varphi ) \rightarrow \exists X^n \varphi } \, (\forall^2E)$$
$${ \forall X^n (\varphi \rightarrow \exists X^n \varphi) \quad ∀X^n(\varphi \rightarrow \exists X^n \varphi ) \rightarrow \exists X^n \varphi \over \exists X^n \varphi} \, (\rightarrow E)$$
Thus :


$\vdash_2 ∀X^0(∀X^n(\varphi \rightarrow X^0) \rightarrow X^0) \rightarrow ∃X^n \varphi$.



Note
For the rules, see page 147; in particular :

$${\varphi^* \over \exists X^n \varphi } \, (\exists^2I)$$

and :

$${\forall X^n \varphi \over \varphi^*} \, (\forall^2E)$$

where 

$\varphi^*$ is obtained from $\varphi$ by replacing each occurrence of $X^n(t_1,\ldots, t_n)$ by $σ(t_1,\ldots, t_n)$ for a certain formula $σ$, such that no free variables among the $t_i$ become bound after the substitution.

A: Coq seems to be happy with this. The easy direction (sigT is $\Sigma$ and forall is $\Pi$):
Parameter V : Type -> Type.

Lemma rabbit : 
  sigT V -> forall Y, (forall X , V X -> Y) -> Y.
Proof.
  firstorder.
Qed.

Print rabbit.

We get the following proof:
  fun (X : sigT V) (Y : Type) (P : (forall Z : Type, V Z -> Y)) =>
    sigT_rect (fun _ : sigT V => Y)
              (fun (x : Type) (p : V x) =>
                 (fun X1 : V x -> Y => (fun X2 : Y => X2) (X1 p)) (P x)) X.

where sigT_rect is the eliminator for $\Sigma$. But you asked about the converse:
Lemma fox : 
  (forall Y, (forall X , V X -> Y) -> Y) -> sigT V.
Proof.
  intro H.
  apply H.
  intros X Y.
  exists X.
  exact Y.
Qed.

Print fox.

The proof found is
  fun H : (forall Y : Type, (forall X : Type, V X -> Y) -> Y) =>
    H (sigT V) (fun (X : Type) (Y : V X) => existT V X Y)

This is quite simple, actually, here's a translation. Suppose
$$H : \Pi Y \,.\, (\Pi X \,.\,(V X \to Y)) \to Y$$
Then $G = H \,(\Sigma Z \,.\, V Z)$ has the type
$$(\Pi X \,.\, (V X \to (\Sigma Z \,.\, V Z))) \to (\Sigma Z \,.\, V Z)$$
and so we just have to apply $G$ to a function of type
$$\Pi X \,.\, (V X \to (\Sigma Z \,.\, V Z))$$
Such a function is
$$\lambda X \,.\, \lambda W \,.\, (X, W)$$
i.e., the dependent pairing function.
