proposition: Lemma ProdBag_BagCountCorrect : BagCountCorrect ProdBag_RepInv ProdBag_bcount ProdBag_bfind.
proof: Proof. unfold ProdBag_bcount, ProdBag_bfind, BagCountCorrect. intros container st [repA [repB repP] ]. destruct Prod_st_choice; eapply bcount_correct; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties