proposition: Lemma EnsembleComplementIntersection {A} : forall E (P : Ensemble A), DecideableEnsemble P -> forall (a : @IndexedElement A), (In _ (Intersection _ E (Complement _ (EnsembleDelete E P))) a <-> In _ (Intersection _ E (fun itup => P (indexedElement itup))) a).
proof: Proof. unfold EnsembleDelete, Complement, In in *; intuition; destruct H; constructor; eauto; unfold In in *. - case_eq (DecideableEnsembles.dec (indexedElement x)); intros. + eapply dec_decides_P; eauto. + exfalso; apply H0; constructor; unfold In; eauto. intros H'; apply dec_decides_P in H'; congruence. - intros H'; destruct H'; unfold In in *; 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