[TYPES] Parametricity for F-omega

[Richard Nathan Linger]

Is there a parametricity theorem for F-omega?  
Any references are welcome.

More specifically,
  if the relation arising from the type Int is defined by
  	i R_{Int} j   iff   i=j

  and the relation arising from the type AxB is defined by
  	(x,y) R_{AxB} (x',y')   iff   x R_A y  &  x' R_B y'

  then what is the relation arising from the type A B, 
    where A and B are types of kind * -> * and * 
    (more generally, of kind k1 -> k2 and k1), 
    respectively?

Nathan Linger