Hola.
Antes de aplicar el absurdo, fijate que tenés en particular las hipótesis O=n y exists m :nat, n = (S m).
Deberías hacer la eliminación de la hipótesis que tiene el existe y luego ver como llegar a un absurdo con las hipótesis que se generan.
El axioma disc puede ser útil :)
Saludos, Carlos