proposition: Lemma In_UnConstrQuery_In {qsSchema} {A} : forall (qs : UnConstrQueryStructure qsSchema) Ridx bod results, UnConstrQuery_In qs Ridx bod ↝ results -> forall (a : A), List.In a results -> exists (tup' : IndexedRawTuple) results', Ensembles.In _ (GetUnConstrRelation qs Ridx) tup' /\ bod (indexedElement tup') ↝ results' /\ List.In a results'.
proof: Proof. unfold UnConstrQuery_In, QueryResultComp; intros; computes_to_inv. unfold UnIndexedEnsembleListEquivalence in *; destruct_ex; intuition; subst. rewrite map_map in H'. remember (GetUnConstrRelation qs Ridx); clear Heqi; revert i a results H0 H' H H3; induction x; simpl in *; intros; computes_to_inv; subst. - simpl in H0; intuition. - apply in_app_or in H0; intuition. exists a; exists v; intuition; try eapply H; eauto. inversion H3; subst. destruct (IHx (fun tup => tup <> a /\ i tup) _ _ H1 H''); eauto. unfold Ensembles.In; intros; intuition; subst; eauto. eapply H in H6; intuition. apply H4; apply in_map; auto. apply H; intuition. destruct_ex; intuition. eexists x0, x1; intuition. apply H2. Qed.
imports: Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query Coq.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool Coq.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.Computation.Refinements.General Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Operations.Mutate