proposition: Lemma IndexedBag_BagDeleteCorrect : BagDeleteCorrect IndexedBag_RepInv IndexedBag_bfind Matcher IndexedBag_benumerate IndexedBag_bdelete.
proof: Proof. unfold BagDeleteCorrect, IndexedBag_benumerate, IndexedBag_bdelete. intros [ibag pool] st rep. pose proof (IndexedBag_bdelete_Preserves_RepInv _ st rep) as rep_del. destruct rep as [repi repp]; destruct rep_del as [_ repp_del]. rewrite surjective_pairing with (p:=ibdelete ibag st); split; simpl in *. - admit. - admit. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.Structures.OrderedTypeEx