Here's a count function defined via fold, using the supplementary [eqf]. ``` Definition eq_cor {X : Type} (eqf : X -> X -> bool) := forall (x y : X), x = y <-> eqf x y = true. Definition count_fold {X: Type} {eqf} : @eq_cor X eqf -> X -> list X -> nat := fun _ x l => (fold X nat (fun y n => if eqf x y then n + 1 else n) l 0). ``` With [count_fold], I would like to prove these 2 theorems below. First: ``` Theorem count_fold_nil {X : Type} {eqf} : forall (l : list X) (eq: eq_cor eqf), (forall (x:X), count_fold eq x l = 0) <-> l = nil. ``` A hint for this: I might need to prove a little lemma for one of directions: for example, that n <> S n for any n. Of course, it may also be the case that there is such a lemma in the standard library. What I tried, is to prove by induction on l, but I'm stuck. Second: ``` Theorem count_occ_cons_eq {X : Type} {eqf} : forall (l : list X) (eq: eq_cor eqf) (x y : X), x = y <-> count_fold eq y (x::l) = S (count_fold eq y l). ``` I tried unfolding [count_fold], it didn't help. By the way, this is how [fold] is defined: ``` Print fold_right. fun (A B : Type) (f : B -> A -> A) (a0 : A) => fix fold_right (l : list B) : A := match l with | [] => a0 | b :: t => f b (fold_right t) end : forall A B : Type, (B -> A -> A) -> A -> list B -> A ``` ``` Definition fold (A B: Type) f l b:= @fold_right B A f b l. ``` Thank you in advance.