even more LTL simplification for GF formulas
we could implement those rules:
GF(a & Fb) = G(Fa & Fb)
GF(a & XXXXXFb) = G(Fa & Fb)
GF(a & eventual) = G(Fa & eventual)
we could implement those rules:
GF(a & Fb) = G(Fa & Fb)
GF(a & XXXXXFb) = G(Fa & Fb)
GF(a & eventual) = G(Fa & eventual)