proposition: Lemma flatten_CompList_singleton {A}: forall P, forall middle (head: A), flatten_CompList (map (boxed_option P) middle) ↝ [head] -> exists x, List.In x middle /\ flatten_CompList (map (boxed_option P) [x]) ↝ [head].
proof: Proof. induction middle; unfold flatten_CompList; simpl; intros. - computes_to_inv; discriminate. - computes_to_inv. destruct v. + rewrite app_nil_l in H''; subst. destruct (IHmiddle _ H') as [ x (x_in & flat_comp) ]. eexists; eauto. + rewrite <- app_comm_cons in H''; injection H''; intros. symmetry in H0; rewrite app_eq_nil_iff in H0; destruct H0; subst. exists a; repeat (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