proposition: Lemma refine_flatten_CompList_func' : forall (A B : Type) (l : list A) (f f' : A -> Comp (list B)), (forall v, List.In v l -> refine (f v) (f' v)) -> refine (flatten_CompList (map f l)) (flatten_CompList (map f' l)).
proof: Proof. induction l; simpl; intros. - reflexivity. - rewrite H by eauto. f_equiv; intro. rewrite IHl by eauto. reflexivity. Qed.
imports: Coq.Lists.List Coq.Program.Program Coq.Sets.Ensembles Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.ListMorphisms Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation