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 ] , []