proposition: Lemma get_update_unconstr_iff {db_schema qs table new_contents} : forall x, Ensembles.In _ (GetUnConstrRelation (@UpdateUnConstrRelation db_schema qs table new_contents) table) x <-> Ensembles.In _ new_contents x.
proof: Proof. unfold GetUnConstrRelation, UpdateUnConstrRelation, EnsembleInsert. intros. rewrite ith_replace2_Index_eq; reflexivity. 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