fact: Definition BagCountCorrect {TContainer TItem TSearchTerm: Type} (RepInv : TContainer -> Prop) (bcount : TContainer -> TSearchTerm -> nat) (bfind : TContainer -> TSearchTerm -> list TItem) := forall container search_term (containerCorrect : RepInv container), List.length (bfind container search_term) = (bcount container search_term).
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Program.Program Coq.Sorting.Permutation