fact: Definition ProperAttributeToCorrectBag {heading} TBag TSearchTerm TUpdateTerm (TBagAsBag : Bag TBag (@RawTuple heading) TSearchTerm TUpdateTerm) (RepInv : TBag -> Prop) (ValidUpdate : TUpdateTerm -> Prop) (TBagAsCorrectBag : CorrectBag RepInv ValidUpdate TBagAsBag) (pattr : @ProperAttribute heading) : CorrectBag (ProperAttributeToRepInv _ _ _ RepInv TBagAsBag pattr (ProperAttributeToProjection pattr)) (ProperAttributeToValidUpdate _ _ _ ValidUpdate TBagAsBag pattr (ProperAttributeToProjection pattr)) (ProperAttributeToBag TBag TSearchTerm TUpdateTerm TBagAsBag pattr) := match pattr as pattr' return CorrectBag (ProperAttributeToRepInv _ _ _ RepInv TBagAsBag pattr' (ProperAttributeToProjection pattr')) (ProperAttributeToValidUpdate _ _ _ ValidUpdate TBagAsBag pattr' (ProperAttributeToProjection pattr')) (ProperAttributeToBag TBag TSearchTerm TUpdateTerm TBagAsBag pattr') with | {| Attribute := attr; ProperlyTyped := inleft (inleft (left cast')) |} => NTreeBag.IndexedBagAsCorrectBag TBagAsBag RepInv ValidUpdate TBagAsCorrectBag (fun x => cast cast' (GetAttributeRaw x attr)) | {| Attribute := attr; ProperlyTyped := inleft (inleft (right cast')) |} => ZTreeBag.IndexedBagAsCorrectBag TBagAsBag RepInv ValidUpdate TBagAsCorrectBag (fun x => cast cast' (GetAttributeRaw x attr)) | {| Attribute := attr; ProperlyTyped := inleft (inright cast') |} => NatTreeBag.IndexedBagAsCorrectBag TBagAsBag RepInv ValidUpdate TBagAsCorrectBag (fun x => cast cast' (GetAttributeRaw x attr)) | {| Attribute := attr; ProperlyTyped := inright cast' |} => StringTreeBag.IndexedBagAsCorrectBag TBagAsBag RepInv ValidUpdate TBagAsCorrectBag (fun x => cast cast' (GetAttributeRaw x attr)) end.
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