proposition: Lemma flatten_CompList_nil {A} : forall (P : Ensemble A) (P_dec : DecideableEnsemble P) (As : list A), FlattenCompList.flatten_CompList (map (fun a : A => Query_Where (P a) (Query_Return a)) As) ↝ nil -> forall a, List.In a As -> ~ P a.
proof: Proof. induction As; simpl; intros; computes_to_inv; subst; simpl in *; intuition. unfold Query_Where, Query_Return in H; computes_to_inv; intuition. destruct (dec a) eqn: ?. - rewrite dec_decides_P in Heqb. apply H0 in Heqb; computes_to_inv; subst; simpl in *; subst; intuition eauto. discriminate. - subst; apply H0 in H1; computes_to_inv; subst; simpl in *; subst; intuition eauto. discriminate. - eapply IHAs; eauto. apply app_eq_nil in H''; intuition; subst; eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Operations.Empty