Hola.
La función deleteAll está bien definida.
En la parte de la prueba donde están perdieron (falta) en como hipótesis información sobre la comparación entre "x" y "a". De hecho, con las hipótesis que están no es posible demostrar el goal ya que falta en este caso la información que "x" es distinto de "a" (sino, no vale).
Cuando hagan el análisis de casos sugiero usar en vez de "destruct (equal x a)", lo siguiente: "case_eq (equal x a)". De esta manera, para ambos casos se genera la hipótesis correspondiente: "equal x a = true" y "equal x a = false".
Saludos, Carlos