proposition: Corollary For_In_Where_Prop {qs_schema} : forall idx r_o P l, DecideableEnsemble P -> Query_For (Query_In (qs_schema := qs_schema) r_o idx (fun r : RawTuple => Query_Where (P r) (Query_Return r) )) ↝ l -> Forall P l.
proof: Proof. unfold Query_In, Query_For, QueryResultComp; intros; computes_to_inv. apply Forall_forall; intros. eapply flatten_CompList_Prop in H'0; eauto. symmetry in H'. eapply Permutation_in; 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