proposition: Lemma IndexedBag_BagUpdateCorrect : BagUpdateCorrect IndexedBag_RepInv IndexedBag_ValidUpdate IndexedBag_bfind Matcher IndexedBag_benumerate Transform IndexedBag_bupdate.
proof: Proof. unfold BagUpdateCorrect, IndexedBag_benumerate, IndexedBag_bupdate. simpl; intros [ibag pool] st ut [repi repp]; split; simpl. - 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