fact: Definition BagDeleteCorrect {TContainer TItem TSearchTerm: Type} (RepInv : TContainer -> Prop) (bfind : TContainer -> TSearchTerm -> list TItem) (bfind_matcher : TSearchTerm -> TItem -> bool) (benumerate : TContainer -> list TItem) (bdelete : TContainer -> TSearchTerm -> (list TItem) * TContainer) := forall container search_term (containerCorrect : RepInv container), Permutation (benumerate (snd (bdelete container search_term))) (snd (List.partition (bfind_matcher search_term) (benumerate container))) /\ Permutation (fst (bdelete container search_term)) (fst (List.partition (bfind_matcher search_term) (benumerate container))).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Program.Program Coq.Sorting.Permutation