fact: CoInductive ACProcess : Set := | ACTALK : forall c1 : Chnl, A c1 -> ACProcess -> forall c2 : Chnl, (A c2 -> ACProcess) -> ACProcess | ACLISTEN : forall c : Chnl, (A c -> ACProcess) -> ACProcess | ACPAR : ACProcess -> ACProcess -> ACProcess.