Let x be given.

Assume Hx.

Apply Sing_nat_fresh_extension 2 nat_2 In_1_2 x to the current goal.

We will prove ExtendedSNoElt_ 2 x.

An exact proof term for the current goal is SNo_ExtendedSNoElt_2 x Hx.

∎