Let Y and x be given.

Apply Empty_eq to the current goal.

Let u be given.

Assume Hu.

Apply SNo_sqrtauxset_E Y 0 x u Hu to the current goal.

Let y be given.

Assume Hy: y ∈ Y.

Let z be given.

Assume Hz: z ∈ 0.

We will prove False.

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

∎