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 (FlattenCompList.flatten_CompList (map f l)) (FlattenCompList.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: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.SumType Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Bedrock.Word Bedrock.Memory