module Tagged where
open import GeneralLemmas hiding ([_])
open import Data.List using ([_])

data Tagged (Msg : Set) : Set where
  silent   : Tagged Msg
  send     : Msg  Tagged Msg
  receive  : Msg  Tagged Msg

detag :  {A : Set}  Tagged A  List A × List A
detag silent       = []     , []
detag (send x)     = []     , [ x ]
detag (receive x)  = [ x ]  , []