proposition: Lemma flatten_CompList_nil {A} : forall (P: A -> Prop), forall (seq : list (@IndexedElement A)), flatten_CompList (map (boxed_option P) seq) ↝ [] -> forall x, List.In x seq -> (~ P (indexedElement x)).
proof: Proof. induction seq; simpl; intros flatten_comp * in_seq. - exfalso; assumption. - computes_to_inv; subst. symmetry in flatten_comp''; rewrite app_eq_nil_iff in flatten_comp''; destruct flatten_comp''; subst. destruct in_seq; subst. + apply boxed_option_nil; assumption. + apply IHseq; assumption. 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