proposition: Lemma DeletedTuplesIntersection {qsSchema} : forall qs Ridx (P : Ensemble RawTuple), DecideableEnsemble P -> refine {x | @QSDeletedTuples qsSchema qs Ridx P x} {x | UnIndexedEnsembleListEquivalence (Intersection _ (GetUnConstrRelation qs Ridx) (fun itup => P (indexedElement itup))) x}.
proof: Proof. intros qs Ridx P P_dec v Comp_v; computes_to_inv. computes_to_constructor. unfold QSDeletedTuples, UnIndexedEnsembleListEquivalence in *; destruct_ex; intuition; subst. eexists; intuition. unfold EnsembleListEquivalence in *; intuition; eauto with typeclass_instances. + eapply H; eapply EnsembleComplementIntersection; eauto with typeclass_instances. + eapply EnsembleComplementIntersection; eauto with typeclass_instances. eapply H; eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.List.ListFacts Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.Schema Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Mutate Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.DecideableEnsembles Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.MutateRefinements Fiat.Common.Ensembles.EnsembleListEquivalence