How to prove the equivalence between Hoare and Floyd assignment axioms?
but when I try $F = G[v/e]$ then from $\exists v' (F[v/v'] \land v=e[v/v'])$ I can't obtain $G$.


We can assume $v'$ not free in $G$. Then, we have

$$
\begin{array}{ll}
&amp; \exists v' (F[v/v'] \land v=e[v/v']) \\
\iff &amp; \mbox{\{def. $F$\}}\\
&amp; \exists v' (G[v/e][v/v'] \land v=e[v/v']) \\
\iff &amp; \mbox{\{property of $H[v/-][v/-]$\}}\\
&amp; \exists v' (G[v/(e[v/v'])] \land v=e[v/v']) \\
\iff &amp; \mbox{\{replacing equals with equals\}}\\
&amp; \exists v' (G[v/v] \land v=e[v/v']) \\
\iff &amp; \mbox{\{$[v/v]$ has no effect\}}\\
&amp; \exists v' (G \land v=e[v/v']) \\
\iff &amp; \mbox{\{$v'$ not free in $G$\}}\\
&amp; G \land \exists v' (v=e[v/v']) \\
\implies &amp; \mbox{\{logic\}}\\
&amp; G
\end{array}
$$

The crucial step is to realize that any $v$ which occurs free in $G[v/e]$ is a $v$ that originated from $e$. Hence, $G[v/e][v/t] = G[v/(e[v/t])]$.

Also note that we don't get exactly $G$ but a slightly stronger postcondition. Since postconditions can be weakened, this is not an issue.