Hola Bruno.
En definiciones propias es así. En este caso nil tiene un argumento -en la definción de list- aunque puede deducir el tipo.
Por ahora es mejor que trabajen poniendo todos los parámetros que corresponden, aunque se puede trabajar con argumentos implícitos en Coq (ver por ejemplo en https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html).
De hecho, en el ejemplo que diste, usando las listas predefinidas en Coq, es posible escribir:
Fixpoint member (n:nat)(l: list nat) :=
match l with
nil => false
Saludos, Carlos