Proper instance for heterogeneous ssim

[nchappe]

A property stating that if L == L' then ssim L == ssim L' would be useful (L and L' are relations on labels).

In 5537188 I introduced an admitted instance gfp_weq, I don't think this is provable without delving into the definitions of gfp/t from coq-coinduction.

Not sure but the theorem may also be true with <= instead of ==.