Winning strategies descend through game coverings

Let $x$ be any maximal play consistent with $\varphi (\sigma )$. F1 gives a maximal $\sigma$-consistent lift $y$ with $\pi (y)\subseteq x$. Since $\sigma$ wins, $y$ is not taboo for $P$. The losing-short-lift alternative is therefore impossible, so $\pi (y)=x$.

If $y$ is infinite, $x$ is infinite by length preservation. When $P=I$, winning gives $y\in {\pi }^{-1}(A)$, hence $x\in A$. When $P=II$, winning gives $y\mathrm{\notin }{\pi }^{-1}(A)$, hence $x\mathrm{\notin }A$. Thus $x$ wins for $P$ in either case.

If $y$ is finite, equality in step 1.1 makes $x$ finite and maximal, hence a terminal taboo. If it were taboo for $P$, reflection F1 would make $y$ taboo for $P$, contrary to its winning status. The terminal partition therefore labels $x$ taboo for the opponent, so it wins for $P$. Every consistent maximal $x$ has now been treated, proving the asserted winning strategy. QED.