fact: Fixpoint foldComp `(f : A -> B -> Comp A) (s : A) (l : list B) : Comp A := match l with | nil => ret s | cons y ys => f s y >>= fun s' => foldComp f s' ys end.
imports: Fiat.Common Fiat.Computation.Core Fiat.Computation.SetoidMorphisms