proposition: Lemma CountingListMap_consistent (container: CountingList) (cconsistent : CountingList_RepInv container) (update_f : TItem -> TItem) : length (List.map update_f (ccontents container)) = clength container.
proof: Proof. rewrite List.map_length; auto using cconsistent. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts