proposition: Lemma ProdBag_BagMatcherEquiv : forall st i, ProdBag_bfind_matcher st i = bfind_matcher Prod_st_A i.
proof: Proof. intros st i; unfold ProdBag_bfind_matcher. destruct Prod_st_choice; try rewrite Prod_st_proof; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties