I misspoke: even the implication
[](\E x : F) => \EE x : []F
is not valid in general, but it is valid if F is a state predicate, or somewhat more generally, if x does not occur in the scope of temporal operators. For example, assume that v is a state variable, then
[](\E x : x = v /\ \E y : [](x=y))
is valid (it suffices at every instant to take x = v, y=x and since both x and y are rigid variables their values never change), but the formula
\EE x : [](x = v /\ \E y : [](x=y))
will not hold in general: the first conjunct requires that x and v always have the same value, but the second conjunct requires that x remains constant, which is impossible if v changes during the behavior.
For an arbitrary formula F(x), we only have
[](\E x : F(x)) => \EE x : [](\E y : y=x /\ F(y))
but this formula does not appear to be very useful.
Sincere apologies: temporal quantifiers are really delicate!
Stephan