proposition: Lemma CountingList_BagCountCorrect : BagCountCorrect CountingList_RepInv CountingListAsBag_bcount CountingListAsBag_bfind.
proof: Proof. unfold BagCountCorrect, CountingListAsBag_bcount, CountingListAsBag_bfind, CountingList_RepInv; intros; pose proof (CountingList_BagCountCorrect_aux (ccontents container) search_term 0) as temp; rewrite Nat.add_0_r in temp; simpl in temp. simpl; [ apply temp ]. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts