Hola.
Cómo definiste isSet? Podés definir inductivamente esta relación La lista vacía debería estar en isSet y, para una lista no vacía, cons x l: se debería cumpir que x no esté en l e isSet(l).
De H deberías poder deducir que x no pertenece a l (con inversion). Luego, de esto y H0 tendrías False, para probar el goal.
Saludos, Carlos