proposition: Lemma flatten_CompList_app_cons_inv {A}: forall P, (forall a, P a \/ ~ P a) -> forall x1 x0_before (head: A) x0_after, flatten_CompList (map (boxed_option P) x1) ↝ (x0_before ++ head :: x0_after) -> exists x1_before x1_middle head' x1_after, x1 = x1_before ++ x1_middle ++ x1_after /\ List.In head' x1 /\ flatten_CompList (map (boxed_option P) x1_before) ↝ x0_before /\ flatten_CompList (map (boxed_option P) [head'] ) ↝ [head] /\ flatten_CompList (map (boxed_option P) x1_after ) ↝ x0_after.
proof: Proof. intros. apply flatten_CompList_app_inv in H0; try assumption. destruct H0 as [ x1_before [ x1_after (eq_split & comp1 & comp2) ] ]; subst. rewrite <- app_singleton in comp2; apply flatten_CompList_app_inv in comp2; try assumption. destruct comp2 as [ middle [ x1_after' (eq_split' & comp2 & comp3) ] ]; subst. apply flatten_CompList_singleton in comp2. destruct comp2 as [ head' (in_middle & comp2) ]. repeat setoid_rewrite in_app_iff. eexists _, _ ,_ ,_; repeat split; intuition; try eassumption; intuition. 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