proposition: Lemma flatten_CompList_app : forall {A} x1 x2 x1' x2', flatten_CompList x1 ↝ x1' -> flatten_CompList x2 ↝ x2' -> @flatten_CompList A (x1 ++ x2) ↝ (x1' ++ x2').
proof: Proof. induction x1; simpl; intros. computes_to_inv; subst. rewrite !app_nil_l; assumption. computes_to_inv. specialize (IHx1 x2 _ _ H' H0). repeat (computes_to_econstructor; eauto). subst; rewrite app_assoc; constructor. 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