proposition: Lemma refine_foldComp : forall (A B : Type) (s : A) (l : list B) (f g : A -> B -> Comp A), pointwise_relation2 refine f g -> refine (foldComp f s l) (foldComp g s l).
proof: Proof. intros. subst. f_equiv. unfold pointwise_relation2 in H. intros st0 st1 Hst x0 x1 Hx. rewrite H. subst. reflexivity. Qed.
imports: Fiat.Common Fiat.Computation.Core Fiat.Computation.SetoidMorphisms