proposition: Lemma flatten_CompList_ret: forall (A B : Type) (f : A -> B) (l : list A), refine (ret (map f l)) (FlattenCompList.flatten_CompList (map (fun a => ret [(f a)]) l))%list.
proof: Proof. induction l; simpl. - reflexivity. - setoid_rewrite <- IHl. repeat setoid_rewrite refineEquiv_bind_unit. simpl; 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