proposition: Corollary binsertPlus_correct_DB : forall {db_schema : RawQueryStructureSchema} qs (index : Fin.t _) (bag_plus : BagPlusProof RawTuple) store, GetUnConstrRelation qs index ≃ store -> forall tuple bound (ValidBound : UnConstrFreshIdx (GetUnConstrRelation qs index) bound), GetUnConstrRelation (@UpdateUnConstrRelation db_schema qs index (EnsembleInsert {| elementIndex := bound; indexedElement := tuple |} (GetUnConstrRelation qs index))) index ≃ binsert (Bag := BagPlus bag_plus) store tuple.
proof: Proof. simpl; intros; constructor. - eapply binsert_correct_DB; eauto. - eapply binsert_RepInv; apply H. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Coq.Lists.List Coq.Program.Program Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.NArith.BinNat Coq.ZArith.ZArith_dec Coq.Arith.Arith Coq.FSets.FMapAVL Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.List.ListQueryRefinements