open :: Path -> File | Error

Theorem open_opens : forall f p, open p == value f, Opened f.

read :: forall file, Opened file -> String -> Opened file * string

close :: forall file, Opened file -> File

Theorem close_closes : forall f, Closed (close f).