proposition: Corollary bemptyPlus_correct_DB : forall {db_schema : RawQueryStructureSchema} {index : Fin.t _} {bag_plus : BagPlusProof (@RawTuple _)}, GetUnConstrRelation (imap2 rawRel (Build_EmptyRelations (qschemaSchemas db_schema))) index ≃ bempty (Bag := BagPlus bag_plus).
proof: Proof. destruct bag_plus; intros; simpl; constructor. eapply bempty_correct_DB; eauto. apply bempty_RepInv. 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