Let z be given.

Assume Hz.

Apply Sing_nat_fresh_extension 3 nat_3 In_1_3 z to the current goal.

We will prove ExtendedSNoElt_ 3 z.

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

∎