Symmetry lemma for forcing automorphisms

Simultaneously induct on the ranks of $\sigma ,\tau$. In the atomic membership and equality clauses, $q\le p$ iff $\pi q\le \pi p$, compatible extensions correspond under $\pi$, and subnames correspond rank-preservingly. Therefore $p⊩\sigma \in \tau$ iff $\pi p⊩\pi \sigma \in \pi \tau$, and likewise for equality.

Induct on formula complexity. Boolean clauses commute with the bijection of conditions. For an existential, F1 maps the class of all $P$-names bijectively to itself, so witnesses correspond; applying the inverse automorphism from F1 gives the reverse implication. This is a syntactic induction on the stated forcing clauses; no semantic-generic existence hypothesis is used.

Now assume $\pi \in G$ and $\vec{\tau }\in \mathrm{H}\mathrm{S}$. F4 makes $\pi \vec{\tau }$ an HS tuple. Apply the already-proved ordinary forcing equivalence of step 2.1 to these parameter tuples; its existential name quantifier still ranges over all $P$-names, exactly as F3 specifies. This proves the asserted parameter-preserving specialization and makes no claim about an unintroduced HS-restricted forcing relation.