Hola.
En lo primero que ponés fijate que en H tenés UTIL (al eliminar el /\) y ~UTIL (H0). De ambos surge una contradicción; desde el punto de vista lógico, de False se deduce cualquier cosa.
Al hacer absurd(UTIL) se pide probar UTIL y ~UTIL para probar el goal.
Otra opción seía elim(H0 H_UTIL), donde H_UTIL sería una prueba de UTIL (que surge al desarmar H). Notar que este elim se aplica a False ya que (H0 H_UTIL) es False (recordar que ~X es X->False).
Espero esto aclare tus dudas.
Saludos, Carlos