\begin{circuslaw}{extchoice-par-intro}
\begin{circusaction*}
  ((c \then A_1) \circseq A_2) \lpar ns_1 | cs | ns_2 \rpar (c \then A_3) \; \equiv
  \also
  (((c \then A_1) \extchoice (c_1 \then B_1) \extchoice ~ \dots ~ \extchoice (c_n \then B_n)) \circseq A_2) \lpar ns_1 | cs | ns_2 \rpar (c \then A_3)
  \also
  \provided \; c \in cs \; \provand \; \mbox{$c$ is distinct from all $c_i$~(the $B_i$ can be chosen arbitrarily)}
\end{circusaction*}
\end{circuslaw}
