proposition: Lemma DropQSConstraints_AbsR_SatisfiesTupleConstraints : forall {qs_schema} r_o r_n, @DropQSConstraints_AbsR qs_schema r_o r_n -> forall idx tup tup', elementIndex tup <> elementIndex tup' -> GetUnConstrRelation r_n idx tup -> GetUnConstrRelation r_n idx tup' -> SatisfiesTupleConstraints idx (indexedElement tup) (indexedElement tup').
proof: Proof. intros. rewrite <- H in *. unfold SatisfiesTupleConstraints, GetNRelSchema, GetUnConstrRelation, DropQSConstraints in *. generalize (rawTupleconstr (ith2 (rawRels r_o) idx)). rewrite <- ith_imap2 in *. destruct (tupleConstraints (Vector.nth (qschemaSchemas qs_schema) idx)); eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Update Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements