[TYPES] how to typing for logic equality operator

[朱常鹏]

I am reading the 19th chapter of Types and Programming Languages.
I encounter a problem during adding a typing rule for logic equality operator == to FJ.
According to the Java  equality operator semantic, the typing rule seems to be described as follow: 
e1 : T1  e2 : T2  T1 <: T2 || T2 <: T1
--------------------------------
e1 == e2 : Bool
However, term substitution doesn't preserve the typing rule, since the relation T1' <: T2' || T2' <: T1'
may be not hold after a substitution, where [x ->s]e1 : T1' and [x->s]e2 : T2'.

who can help me to solve the problem, thank you in advance.