proposition: Lemma refine_Iterate_MutationPreservesCrossConstraints : forall qsSchema qs Ridx MutatedTuples or, @DropQSConstraints_AbsR qsSchema or qs -> ((forall Ridx', Ridx' <> Ridx -> forall tup' : IndexedRawTuple, GetRelation or Ridx tup' -> SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup') (GetUnConstrRelation (DropQSConstraints or) Ridx')) -> forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints MutatedTuples (GetUnConstrRelation (DropQSConstraints or) Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx')) -> Iterate_Ensemble_BoundedIndex_filter (fun Ridx' => forall tup' : IndexedRawTuple, GetUnConstrRelation (DropQSConstraints or) Ridx tup' -> SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup') (GetRelation or Ridx')) (fun idx => if fin_eq_dec Ridx idx then false else true) -> forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints MutatedTuples (GetRelation or Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx').
proof: Proof. intros; rewrite <- GetRelDropConstraints in *; eapply H0; eauto. intros; rewrite GetRelDropConstraints in *. intros; eapply (proj1 (Iterate_Ensemble_BoundedIndex_filter_equiv _ (Build_DecideableEnsemble _ _ (ibound_check_dec _) )) H1); try 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.Common.Ensembles.IndexedEnsembles Fiat.Common.ilist2 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.QueryStructure.Specification.Operations.Query 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.Common.Ensembles.EnsembleListEquivalence