Hola.
No se qué versión estás usando, pero a mi me funciona:
Variable A:Set.
Inductive eq_list: list A -> list A -> Prop :=
eq_list0 : eq_list nil nil
| eq_listS : forall x y xl yl, eq x y -> eq_list xl yl -> eq_list (cons y yl)(cons x xl).
Probá en todo caso poniendo como primera línea:
Set Implicit Arguments.
El mensaje de error que te reporta es porque la lista está definida para elementos de un tipo genérico. Si ponés (nil A) en vez de nil el mensaje de error que te da sobre este constructor (que a mi no me aparece) desaparecería (lo mismo te va a pasar con Cons). Set Implicit Arguments (ver manual de Coq) se usa para que Coq infiera cierto tipos en las definiciones, evitando ponerlos en los usos de las definiciones.
Saludos, Carlos