proposition: Lemma CountingList_BagEnumerateEmpty : BagEnumerateEmpty ccontents CountingList_empty.
proof: Proof. firstorder. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts