[TYPES] a counterexample to Plotkin and Abadi's characterization of equivalence at existential type?

[Derek Dreyer]

> Once again, syntactic reasoning locks in mysteries here.  The remark
> following Theorem 7 provides the only way in PAL to show that two terms of a
> an existential type are equal.  So, if you managed to prove that two such
> terms are equal in PAL, you would have constructed a trasitive composition
> of simulation arguments.  So, the property you want follows as a metatheorem
> about PAL.

So how do you show this?  How do you *prove* that simulation is the
only way to prove that two terms of existential type are equal?  I
don't see how it follows from Theorem 7.

> That is indeed right.  For closed types, the "only if" direction is trivial.
> However, for open types, it is not.  You would notice in Theorem 7 the
> additional condition that x and y have to be related by A[S,rho].  That
> plays a significant role.

This is fascinating, but I still don't understand concretely what one
can "do" with the "only if" direction in the case of open types.

Thanks,
Derek