proposition: Lemma QSDeleteSpec_UnConstr_refine_CrossConstraints' : forall qsSchema qs Ridx (DeletedTuples : Ensemble RawTuple) or, @DropQSConstraints_AbsR qsSchema or qs -> refine {b : bool | (forall Ridx', Ridx' <> Ridx -> forall tup', GetUnConstrRelation qs Ridx tup' -> SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup') (GetUnConstrRelation qs Ridx')) -> decides b (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints (EnsembleDelete (GetRelation or Ridx) DeletedTuples) (GetUnConstrRelation qs Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx'))} (ret true).
proof: Proof. unfold MutationPreservesCrossConstraints; intros * AbsR_or_qs v Comp_v. computes_to_econstructor; intros; computes_to_inv; subst; simpl; intros. unfold DropQSConstraints_AbsR in *; eapply H; inversion H1; subst; eauto. rewrite GetRelDropConstraints; 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