module Main

mutual

  data Locked : Type where
    Start  : Locked
    Lock   : Closed -> Locked

  data Closed : Type where
    Close  : Opened -> Closed
    Unlock : Locked -> Closed

  data Opened : Type where
    Open   : Closed -> Opened

module Main

mutual

  data Locked = Start | Lock Closed
  data Closed = Close Opened | Unlock Locked
  data Opened = Open Closed
