proposition: Lemma CountingList_binsert_Preserves_RepInv : binsert_Preserves_RepInv CountingList_RepInv CountingListAsBag_binsert.
proof: Proof. unfold binsert_Preserves_RepInv, CountingList_RepInv; intros; simpl; rewrite containerCorrect; reflexivity. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts