Hola Alejandro.
Veo que estás siguiendo otro camino de prueba. El error en el apply se debe a que no hiciste la eliminación del existe en la hipótesis, para que puedas usar esta información y aparezca tal elemento de tipo U. El absurd que usás es inncesario. Fijate en:
Lemma e32 : Asimetrica -> Irreflexiva.
Proof.
intro.
unfold not.
intro.
elim H0; intros w Hw. (* acá áplico la eliminación del existe; al elemento lo llamo w *)
apply (H w w); assumption. (* o directamente: exact (H w w Hw Hw). *)
Qed.
Saludos, Carlos