The Interchange lemma in the theory of formal languages has a $\Pi_5$ form:
$\forall L$, if $L$ is a context-free language, then
$\exists c$, $c$ is a positive integer, such that
$\forall n\ge 2$, $R\subseteq L\cap\{0,1\}^n$, $2\le m\le n$,
$\exists Z\subseteq R$, $Z=\{z_1,\dots,z_k\}$, $z_i=w_ix_iy_i$, $k\ge \frac{|R|}{c(n+1)^2}$, and lengths $a,b,c$, such that
$\forall i,j$ with $1\le i,j\le k$, [$|w_i|=|w_j|$, etc. etc.]
The most famous application is to let $L$ be the set of not-square-free words, assume it's context-free, and then carefully choose $R$ and $n$ so as to get a contradiction.