proposition: Lemma flatten_CompList_app_inv' {A : Type} : forall (l l' : list (Comp (list A))) v, flatten_CompList (l ++ l') ↝ v -> exists e e', v = app e e' /\ flatten_CompList l ↝ e /\ flatten_CompList l' ↝ e'.
proof: Proof. induction l; simpl; intros. - eexists []; exists v; simpl; intuition. - computes_to_inv; subst. destruct (IHl _ _ H') as [e [e' [v_eq [Comp_l Comp_l'] ] ] ]. rewrite v_eq. eexists (app v0 e), e'; intuition. repeat computes_to_econstructor; 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