While working on the Lists section of Software Foundations, I tried to define member as follows:

Definition member (v:nat) (s:bag) : bool :=
match gt (count v s) 0 with
| False => false
| True => true
end.

I kept getting “Error: This clause is redundant.” After some digging around, I found Adam’s explanation that logical propositions (Prop) such as gt (count v s) 0 are not usable for pattern matching in Gallina (without solving “the halting problem and more”). The easier solution then hit me (duh):

Definition member (v:nat) (s:bag) : bool :=
match count v s with
| O => false
| _ => true
end.

Thankfully, I learned something new about Prop though :).