With count defined through fold, I would like to prove these 2 theorems below.

First:
```
Theorem foldc  {X : Type} {eqfx} : 
  forall (l : list X) (eqx: eq_corx eqfx),
     (forall (x:X), foldc eq x l = 0) <-> l = nil.
```

Second:
```
Theorem conseqcount {X : Type} {eqfx} : 
    forall (l : list X) (eqx: eq_corx eqfx) (x y : X), 
    x = y <-> foldc eqx y (h::t)  = S (foldc eqx y t).
```