proposition: Lemma CountingList_BagFindCorrect : BagFindCorrect CountingList_RepInv CountingListAsBag_bfind apply ccontents.
proof: Proof. intros; unfold BagFindCorrect, CountingListAsBag_bfind; reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts