Hahaha, I really went in the wrong direction, I see. But you didn't make it easy for me to answer also. Now, I see what you are asking, and actually that is an interesting question.
Clearly, Fφ = A∃({q},¬q,q′↔q∨φ,GFq) means that Fφ is equivalent to the given Büchi automaton A∃({q},¬q,q′↔q∨φ,GFq). However, this refers only to the initial point of time. That means you can replace all formulas Fφ with A∃({q},¬q,q′↔q∨φ,GFq) as long as they are not nested in other formulas. For example, if you have [a SB (F c)], this formula is not the one to choose, since the SB operator will ask for F(c) for points of time later than t=0.
Why is that so? The transition relation q′↔q∨φ implements a watchdog that starts initially in state ¬q, and will switch to q as soon as the first occurrence of φ is seen. It never goes back to ¬q afterwards, and therefore only checks Fφ from t=0 on, but not later.
The other formula you mention is based on the equivalence between G[q↔Fφ] and G[q↔φ∨Xq]∧GF[q→φ] which means that q must ALWAYS (!) behave like Fφ provided that we have q↔φ∨Xq in the transition relation, and add GF[q→φ] as a constraint. This allows you to replace Fφ in any context by q, and therefore also F(c) in [a SB (F c)] to [a SB q] (as long as you add q↔φ∨Xq in the transition relation, and add GF[q→φ] as a constraint).
However, you could use my arguments in the answer above to replace [a SB (F c)] with (F a) & (G !c). Here, the subformula (F a) is only evaluated at the initial point of time, so that you could then use also Fφ = A∃({q},¬q,q′↔q∨φ,GFq) to replace it.
So, the short answer is that it depends on whether the formula Fφ you want to replace is evaluated only at the initial point of time (no surrounding temporal operator) or not.
