\begin{circuslaw}{extract-var-rec}
\begin{circusaction*}
  \circmu X \circspot (\circvar v : T \circspot A) ~ \equiv ~ \circvar v : T \circspot (\circmu X \circspot A)
  \also
  \provided \; \mbox{$v$ is initialised before use in $A$}
\end{circusaction*}
\end{circuslaw}
