\procedure{$\O{Send2}(\n{ctr}, \n{msg})$}{
\pcassert (\n{State}[\n{ctr}] \neq \O{none}\left(\O{Tuple[..]}\right)) \\
 \n{state} \gets \O{unwrap}\left(\n{State}[\n{ctr}]\right)\\
\n{return} \stackrel{\mathsf{\tiny{invoke}}}{\gets} \O{Run2}(\n{state}, \n{msg}) \pccomment{Pkg: Prot} \\
\pcparse \n{return} \pcas \left(\begin{array}{c}\n{state}, \n{msg}_\n{}\end{array}\right)\\
 \n{State}[\n{ctr}] \gets \O{some}\left(\n{state}\right)\\
 \pcreturn \n{msg}_\n{}\\
}
