fact: Fixpoint bindFree A B (c : FreeF A) (f : A -> FreeF B) : FreeF B := match c with | retFree a => f a | opr s k => opr s (fun p => bindFree (k p) f) end.
imports: Coq(ssreflect List) Mon(SPropBase SPropMonadicStructures Monoid)