proposition: Lemma ProdBag_BagEnumerateEmpty : BagEnumerateEmpty ProdBag_benumerate ProdBag_bempty.
proof: Proof. unfold ProdBag_benumerate, BagEnumerateEmpty. eapply benumerate_empty. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties