fact: Definition IndexedBag_bdelete (bag : TIndexedBag) (searchterm : TSearchTerm) := let (deleted, ibag) := ibdelete (fst bag) searchterm in (IndexesToItems deleted (snd bag), (ibag, List.fold_right (fun idx p => pput p idx None) (snd bag) deleted)).
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