- ((G a) <-> (G(G a)))
