proposition: Lemma flatten_CompList_app_inv : forall {A} (P : A -> Prop), (forall a, P a \/ ~ P a) -> forall x1 x0_before x0_after, flatten_CompList (map (@boxed_option A P) x1) ↝ (x0_before ++ x0_after) -> exists x1_before x1_after, x1 = x1_before ++ x1_after /\ flatten_CompList (map (boxed_option P) x1_before) ↝ x0_before /\ flatten_CompList (map (boxed_option P) x1_after ) ↝ x0_after.
proof: Proof. intros * excl; induction x1; simpl; intros. - computes_to_inv. rewrite app_eq_nil_iff in H. setoid_rewrite app_eq_nil_iff. eexists; eexists; intuition; subst; intuition constructor. - computes_to_inv. pose proof H; unfold boxed_option in H0. computes_to_inv; destruct H0 as (spec1 & spec2). destruct (excl (indexedElement a)) as [ Ptrue | Pfalse ]; [ specialize (spec1 Ptrue); computes_to_inv | specialize (spec2 Pfalse) ]; subst. + rewrite app_singleton in H''. destruct x0_before as [ | a' x0_before' ] eqn:eq_before; subst. * rewrite app_nil_l in H''. destruct x0_after as [ | a' x0_after]; try discriminate. injection H''; intros; subst. exists (@nil (@IndexedElement A)). eexists; repeat split; eauto; simpl; repeat econstructor; eauto. * rewrite <- app_comm_cons in H''. injection H''; intros; subst. destruct (IHx1 x0_before' x0_after H') as [ x1_before [ x1_after (_eq & comp1 & comp2) ] ]; subst. exists (a :: x1_before); exists x1_after. simpl; repeat split; repeat (first [eassumption | econstructor]). + rewrite app_nil_l in H''; subst. destruct (IHx1 x0_before x0_after H') as [ x1_before [ x1_after (_eq & comp1 & comp2) ] ]; subst. exists (a :: x1_before); exists x1_after. simpl; repeat split; repeat (first [eassumption | econstructor]). 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