An exact proof term for the current goal is (omega_in_R (ordsucc n) (omega_ordsucc n Hn)).