It is known that Laver's ground model definability theorem doesn’t hold for all class forcing notions. That is, if $M$ satisfies ZFC then $M$ is not necessarily definable in $M[G]$, a class forcing extension of $M$. The following is an instructive instance of this fact but I’m not able to understand the proof.
Let $P$ be the Easton support class product forcing over $L$ that adds a Cohen subset to every regular cardinal and let $G\times H$ be $P\times P$-generic over $L$. Consider the model $L[G]$, which is a ground model of $L[G][H]$. The idea is to show that $L[G]$ cannot be definable in $L[G][H]$ by parameters. Suppose $a$ is any set in $L[G][H]$ and suppose toward contradiction that $\varphi (x,a)$ defines the relation $x\in L[G]$ in $L[G][H]$, forced by some condition $p\in P\times P$. Now I would like to define an automorphism $\pi: P\times P\rightarrow P\times P$ such that $\pi (p)=p$ and $\pi (\dot a)=\dot a$ ($\dot a$ is a name for $a$). Moreover, in order to obtain a contradiction we require that $L[\pi (G)]\neq L[G]$ but the formula $\varphi (x,a)$ also define $L[\pi (G)]$, which is absurd.
So my question is: how can be defined the desired automorphism $\pi$?
