[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> As to what you can "do" with the "only if" direction, I don't know. I was > assuming that you had some application in mind since you raised this. The > "only if" directions are essentially stating completeness of the respective > proof rules. So, they could presumably be used to *disprove* that two terms > are related by showing that all possible ways proving them related are > exhausted. What I find surprising and unintuitive somehow is that we have a theorem which could presumably be used for such "disproving" purposes only in the case that the types are open, and not in the specific case when they are closed. (Off the top of my head, I can't think of other examples of this phenomenon, but it's early in the morning for me. ;-) Incidentally, as I wrote before, I don't think the "only if" direction of Theorem 7 is trivial even in the closed types case: it *does* give you the "canonical forms" property that every term of existential type is equal to some "pack X x". It just doesn't seem to give you anything else in that case. Derek > > Cheers, > Uday >
