fact: Definition Free_bind `(k : a -> Free f b) : Free f a -> Free f b := fun x0 => let fix go x := match x with | Pure a => k a | Join _ g h => Join (go \o g) h end in go x0.
imports: Hask.Prelude Hask.Control.Monad