fact: Fixpoint CountingListPartition (contents : list TItem) (search_term : TItem -> bool) : prod CountingList CountingList := match contents with | nil => (CountingList_empty, CountingList_empty) | x :: tl => let (g,d) := CountingListPartition tl search_term in if search_term x then (CountingListAsBag_binsert g x, d) else (g, CountingListAsBag_binsert d x) end.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts