\begin{circuslaw}{extract-var-seq}
\begin{circusaction*}
  (\circvar v : T \circspot A_1) \circseq A_2 ~ \equiv ~ (\circvar v : T \circspot A_1 \circseq A_2)
  \also
  \provided \; \mbox{$v$ is not free in $A_2$}
\end{circusaction*}
\end{circuslaw}
