Maybe we first make some equivalence transformations:

G(!b-> Xa) = G(b | Xa)

and second

F(!b->(a | X a))
= F(b | a | X a)
= (F b) | (F a) | (F X a)

Hence, if we always have b | X a, we have at any point of time t either b or at t+1, we have a. If we should have b at time t, then we have (F b) at any time before t (hence, we have in particular F(b) at time 0). Otherwise, we have a at t+1, and thus, we have F(a) at any point before t+2, and also F(X a) at any point of time before t+1, in particular, (F a) and (F X a) hold therefore at time 0.

Hence, at time 0, we can say that G(b | Xa) implies F(!b->(a | X a)).

Right?