Checks in my classic, lockable door example implemented in Finito. This does not yet contain the documentation of the door in the Haskell version of Finito.