Let z be given.

Assume Hz.

Apply Sing_nat_fresh_extension 4 nat_4 In_1_4 z to the current goal.

We will prove ExtendedSNoElt_ 4 z.

An exact proof term for the current goal is HSNo_ExtendedSNoElt_4 z Hz.

∎