proposition: Lemma flatten_CompList_nil': forall (A B : Type)(seq : list A), refine (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: 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