proposition: Lemma refine_foldComp_invariant' : forall {A S S'} (P : S -> S' -> Prop) (f : S -> A -> Comp S) (f' : S' -> A -> Comp S') (xs : list A) (z : S) (z' : S') ResultT (k : S -> Comp ResultT) (k' : S' -> Comp ResultT), (forall z z', P z z' -> pointwise_relation _ refine (fun a => z'' <- f z a; {z' | P z'' z'}) (fun a => f' z' a)) -> (forall st_n st_n', P st_n st_n' -> refine (k st_n) (k' st_n')) -> P z z' -> refine (st_n <- foldComp f z xs; k st_n) (st_n' <- foldComp f' z' xs; k' st_n').
proof: Proof. induction xs; intros; autorewrite with monad laws. eauto. rewrite <- (H _ _ H1 a), refineEquiv_bind_bind. f_equiv; intros x. apply refine_bind_pick; intros. apply IHxs; eauto. Qed.
imports: Fiat.Common Fiat.Computation.Core Fiat.Computation.SetoidMorphisms Fiat.ADT Coq.Lists.List