lambda-calculus - 根据存在类型编码通用类型？

Question

在 System F 中，类型exists a. P可以被编码为forall b. (forall a. P -> b) -> b任何使用存在的 System F 术语都可以用这种编码来表示，这种编码尊重类型和归约规则。

在“类型和编程语言”中，出现了以下练习：

我们可以根据存在类型对通用类型进行编码吗？

我的直觉说这是不可能的，因为在某种程度上，“存在包装”机制根本不如“类型抽象”机制强大。我如何正式展示这一点？

我什至不确定我需要证明什么才能正式展示这个结果。