[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 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
