proposition: Lemma In_UnConstrQuery_In' {qsSchema} {A} : forall (qs : UnConstrQueryStructure qsSchema) Ridx (bod : RawTuple -> Comp (list A)) results (a : A) (tup' : IndexedRawTuple), Ensembles.In _ (GetUnConstrRelation qs Ridx) tup' -> (forall results', bod (indexedElement tup') ↝ results' -> List.In a results') -> UnConstrQuery_In qs Ridx bod ↝ results -> List.In a results.
proof: Proof. unfold UnConstrQuery_In, QueryResultComp, Ensembles.In; intros. computes_to_inv. unfold UnIndexedEnsembleListEquivalence in *; destruct_ex; intuition; subst. rewrite map_map in H1'. remember (GetUnConstrRelation qs Ridx); clear Heqi; revert i a results H H0 H1 H1' H4; induction x; simpl in *; intros; computes_to_inv; subst. - simpl in *; intuition; eapply H1; eauto. - apply H1 in H; intuition; subst; apply in_or_app; eauto. right; inversion H4; subst. eapply (IHx (fun tup => tup <> a /\ i tup)); eauto. intuition; subst; eauto. apply H5; eauto using in_map. apply H1; eauto. unfold Ensembles.In; intuition; intros; eauto. rewrite H1 in H7; intuition. subst; eauto using in_map. apply H1; eauto. 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