fact: Fixpoint fold `(r : x -> y) {S : Type} `(c : forall s : S, (P s -> y) -> y) (fr : CFree P x) : y := match fr with | CPure x => r x | CJoin s k => c s $ fun t => fold r c (k t) end.
imports: Hask.Prelude Control.Monad Control.Comonad