proposition: Lemma ProdBag_binsert_Preserves_RepInv : binsert_Preserves_RepInv ProdBag_RepInv ProdBag_binsert.
proof: Proof. unfold binsert_Preserves_RepInv, ProdBag_RepInv. intros container item [repA [repB repP] ]; intuition. - eapply binsert_RepInv; eauto. - eapply binsert_RepInv; eauto. - eapply perm_trans; [ eapply binsert_enumerate | ]; eauto. eapply perm_trans; [ | symmetry; eapply binsert_enumerate ]; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties