proposition: Lemma ProdBag_BagFindCorrect : BagFindCorrect ProdBag_RepInv ProdBag_bfind ProdBag_bfind_matcher ProdBag_benumerate.
proof: Proof. unfold ProdBag_bfind, ProdBag_benumerate, ProdBag_bfind_matcher, BagFindCorrect. intros container st [repA [repB repP] ]. destruct Prod_st_choice. eapply bfind_correct; eauto. setoid_rewrite repP. eapply bfind_correct; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties