proposition: Lemma CountingList_BagCountCorrect_aux : forall (container: list TItem) (search_term: TItem -> bool) default, length (List.filter search_term container) + default = List.fold_left (fun (acc : nat) (x : TItem) => acc + (if search_term x then 1 else 0)) container default.
proof: Proof. induction container; intros. + trivial. + simpl; destruct (search_term a); simpl; rewrite <- IHcontainer; simpl; eauto. rewrite (Nat.add_comm 1); eauto using Nat.add_assoc. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts