fact: Definition ProdBag_bempty := (@bempty _ _ _ _ TBag_A, @bempty _ _ _ _ TBag_B).
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties