The negation of EF phi is AG ¬phi. (In words: “Not all paths have a point at which something holds” is the same as “There is a path where at every points the opposite of something holds)

Thus we get AG ¬¬EF a. The double negation cancels itself out. We are left with AGEF a.