August 21, 2018: Prove a LTL formula (FFGa) ↔ (FGa) to be valid

Question

Prove the LTL formula (FFGa) ↔ (FGa) to be valid by applying these steps: Translate the negation of the formula to a symbolic ω-automaton. 

In the solution's acceptance condition there are three GF's conjuncted. First one is GF[a -> q0], this one is clearly Ga's omega translation. The next GF[q1 -> q0] and GF[q2 -> q1] are Fa's translation.

My question is why did we only considered the first part FFGa although the problem asks to translate the negation of whole formula? (after negation of <-> it becomes xor)

https://es.cs.uni-kl.de/teaching/vrs/exams/2018.08.21.vrs/2018.08.21.vrs.solutions.pdf

Update:

Professor answered on https://q2a.cs.uni-kl.de/1835/august-2018-problem-7b-prove-validity-of-ffga-fga

Answer 1

When we make the abbreviations, we first get

1. q0 := Ga with the rest (FFq0) ↔ (Fq0) 
2. q1 := F q0 with the rest (Fq1) ↔ q1 
3. q2 := F q1 with the rest q2 ↔ q1 

So, the answer is that the abbreviations take care of all occurrences of the sub formulas.