proposition: Lemma flatten_CompList_nil': forall (A B : Type)(seq : list A), refine (FlattenCompList.flatten_CompList (map (fun _ => ret nil) seq)) (ret (@nil B)).
proof: Proof. induction seq; simpl; unfold refine; intros; computes_to_inv; subst; eauto. 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