fact: Definition ProdBag_bupdate_transform := bupdate_transform (Bag:=TBag_A).
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties