proposition: Lemma CountingList_BagInsertEnumerate : BagInsertEnumerate CountingList_RepInv ccontents CountingListAsBag_binsert.
proof: Proof. firstorder. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts