Add an example about free monads with assert

An example with assert in a free monad with arbitrary properties, even non-computational, using a notion of successful run. I do if this is practical compared to asserts on boolean expressions and an option monad.

Given that the properties are arbitrary, this kind of monad could also be a way to encode GADTs. We could ask the user to provide an arbitrary equality proof between two types to do arbitrary casts in the match. We can represent impossible branches with an assert false.