In System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b in the sense that any System F term using an existential can be expressed in terms of this encoding respecting the typing and reduction rules.
In "Types and Programming Languages", the following exercise appears:
Can we encode universal types in terms of existential types?
My intuition says that this isn't possible because in some way the "existential packaging" mechanism simply isn't as powerful as the "type abstraction" mechanism. How do I formally show this?
I am not even sure what I need to prove to formally show this result.