proposition: Lemma refine_foldComp_bind : forall (A B : Type) (s : A) (l : list B) (f f' : A -> B -> Comp A) ResultT (k k' : A -> Comp ResultT), pointwise_relation2 refine f f' -> pointwise_relation _ refine k k' -> refine (x <- foldComp f s l; k x) (x <- foldComp f' s l; k' x).
proof: Proof. intros. rewrite refine_foldComp. f_equiv. exact H0. exact H. Qed.
imports: Fiat.Common Fiat.Computation.Core Fiat.Computation.SetoidMorphisms