proposition: Lemma count_eq : forall A (p:A->bool) (P:A->Prop) l, isTrue_pred p P -> count p l = LibList.count P l.
proof: Proof. Proof using. introv E. induction l as [|x l']; simpl; rew_listx. { auto. } { rewrite IHl'. rewrite E. do 2 case_if; try nat_math. } Qed.
imports: TLC(LibTactics LibReflect)