proposition: Lemma refine_foldComp_fold_left : forall A (xs : list A) S (f : S -> A -> Comp S) (z : S), refineEquiv (foldComp f z xs) (fold_left (fun acc x => s <- acc; f s x) xs (ret z)).
proof: Proof. intros. rewrite <- refine_foldComp_fold_left_helper. autorewrite with monad laws. reflexivity. Qed.
imports: Fiat.Common Fiat.Computation.Core Fiat.Computation.SetoidMorphisms Fiat.ADT Coq.Lists.List