An exact proof term for the current goal is (λx H1 ⇒ SingE 0 x H1 (λs _ : set ⇒ x ∈ ordsucc s) (ordsuccI2 x)).