proposition: Lemma ProdBag_bdelete_Preserves_RepInv : bdelete_Preserves_RepInv ProdBag_RepInv ProdBag_bdelete.
proof: Proof. unfold bdelete_Preserves_RepInv, ProdBag_bdelete. intros container st [repA [repB repP] ]. rewrite surjective_pairing with (p:=bdelete (fst container) Prod_st_A). rewrite surjective_pairing with (p:=bdelete (snd container) Prod_st_B). unfold ProdBag_RepInv; intuition. - destruct Prod_st_choice; eapply bdelete_RepInv; eauto. - destruct Prod_st_choice; eapply bdelete_RepInv; eauto. - destruct Prod_st_choice; simpl; (eapply perm_trans; [ eapply bdelete_correct | ]; eauto; eapply perm_trans; [ | symmetry; eapply bdelete_correct ]; eauto; rewrite !ListFacts.partition_filter_neq; apply ListMorphisms.filter_permutation_morphism; eauto; unfold Morphisms.pointwise_relation; intro; f_equal; eapply Prod_st_proof). Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties