Could you please clarify, why this has been done here?
A∃ ({p, q}, ¬q ∧ p, Φ1 ∧ Φ2, FG¬q ∨ FGp)
A∃ ({q, p}, ¬q ∧ p, Φ1 ∧ Φ2, A∃ ({r}, ¬r, r0 ↔ (r ⇒ p | q), FG(¬r ∨ p)))
Can we do the operation like the below instead of the above one?
A∃ ({p, q}, ¬q ∧ p, Φ1 ∧ Φ2, FG[¬q ∨ p])