A property stating that if L == L' then ssim L == ssim L' would be useful (L and L' are relations on labels).
In 553718804a8b8e2224014b58fafaff1f9cb522bf 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 ==.
A property stating that if
L == L'thenssim L == ssim L'would be useful (L and L' are relations on labels).In 553718804a8b8e2224014b58fafaff1f9cb522bf 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==.