better translation or simplification of GF(a & Fb)

G(F(a & Fb)) is equivalent to G(Fa & Fb), yet I know of no translator that is able to translate the first as efficiently as the second.

It gets worse with G(F(a & F(b & Fc))) etc.

Look at the rewriting rules in the LIO2ALBA paper. It has GF(a & Fb) = GFa & GFb as well as GF(a | Gb) = GFa | FGb (to apply in the other direction).