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