Is the encoding of existential types in System F adequate?

Question

This is somewhat related to How to encode a function from an existential type

Existential types can be encoded in System F. If $P$ is any type constructor, not necessarily covariant, then the existential type $\exists t.~P~t$ is encoded as: $$\forall r.~(\forall t.~P~t \to r)\to r $$

Denote this encoding as the type constructor $E : (* \to *) \to *$ that takes any $P : * \to *$ and makes a new type $\exists t.~P~t$ out of $P$.

So, for any type constructor $P$ we define: $$E~P = \forall r.~(\forall t.~P~t \to r)\to r $$

 E P = ∀(r : *) → (∀(t : *) → P t → r) → r

To create values of the type $E~P$, one uses the standard function pack defined as:

 pack : ∀(s : *) → P s → E P
 pack = λ(s : *) → λ(ps : P s) → λ(r : *) → λ(c : ∀(t : *) → P t → r) → c s ps

The main question is: how to show that all values of type $E~P$ can be obtained using pack. This is to show that pack is surjective; or that the encoding is "adequate" and there are no System F functions of type E P that do not correspond to some encapsulated type s and a value ps : P s.

Alternatively, how to show that is not true and to give a counterexample: some System F code for a certain function f : E P with a suitable $P$ such that there are no types s and no values ps : P s satisfying f = pack s ps.

To show that pack is surjective, we may try implementing its left inverse unpack and show that pack (unpack f) == f.

But it does not seem to be possible to extract s and ps from a given value f : E P. Parametricity is built into System F and it prohibits us from getting any specific type out of $\forall r.~(\forall t.~P~t \to r)\to r$. So, if pack is surjective, the unpack function needs to violate parametricity (and cannot be implemented in System F). That may not be a problem if we are somehow able to show that pack is surjective by going outside System F. But at this point I do not see how to proceed with any possible proof.