fact: Definition ProperAttributeToValidUpdate {heading} TBag TSearchTerm TUpdateTerm (ValidUpdate : TUpdateTerm -> Prop) (TBagAsBag : Bag TBag (@RawTuple heading) TSearchTerm TUpdateTerm) (pattr : @ProperAttribute heading) : (@RawTuple heading -> ProperAttributeToFMapKey pattr) -> TUpdateTerm -> Prop := match pattr as pattr' return (@RawTuple heading -> ProperAttributeToFMapKey pattr') -> TUpdateTerm -> Prop with | {| Attribute := attr; ProperlyTyped := inleft (inleft (left cast')) |} => NTreeBag.IndexedBag_ValidUpdate TBagAsBag ValidUpdate | {| Attribute := attr; ProperlyTyped := inleft (inleft (right cast')) |} => ZTreeBag.IndexedBag_ValidUpdate TBagAsBag ValidUpdate | {| Attribute := attr; ProperlyTyped := inleft (inright cast') |} => NatTreeBag.IndexedBag_ValidUpdate TBagAsBag ValidUpdate | {| Attribute := attr; ProperlyTyped := inright cast' |} => StringTreeBag.IndexedBag_ValidUpdate TBagAsBag ValidUpdate 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