[TYPES] how to typing for logic equality operator‏

[Moez A. Abdel-Gawad]

Incidentally, it seems there is a minor (but embarrassing?) typo in the 
FJ paper (only in the TOPLAS version).

The flaw, in Theorem 2.4.3 (FJ Type Soundness), on p. 408, is in the 
last part of the theorem stating that 'C <: D'.

I believe there must be a 'not' (/) over the '<:' symbol.  Otherwise 
(ie, if the condition as stated is true), the (up-)cast subexpression 
could simply evaluate/reduce to 'new C([e])', and would not be a failing 
typecast (as explained close to the end of p.401).

The same error is repeated in Theorem 3.4.3 (FGJ Type Soundness), I 
believe, for 'Phi |- N <: P', on p. 415.

Or am I missing something?

-Moez