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.