\begin{circuslaw}{var-intro}
\begin{circusaction*}
  A(x) ~ \equiv ~ \circvar v : T \circspot v := x \circseq A(v)
  \also
  \provided \; \mbox{$v$ is not free in $A$}
\end{circusaction*}
\end{circuslaw}
