Sure, since AFAFa = AFa implies by negating both sides EGEGb = EGb. For more general things, I would be more pessimistic since there must be some property of the fixpoint that we exploit here. What we do is increasing/decreasing same way in the two nested fixpoints, and as long as that is done, then yes, it should hold. Alternating fixpoints like EGFa are however not of that kind.