Apply SNo_rec_i_eq G to the current goal.

Let x be given.

Assume Hx.

Let g and h be given.

Assume Hgh.

We will prove SNoCut (⋃_{k ∈ ω}SNo_sqrtaux x g k 0) (⋃_{k ∈ ω}SNo_sqrtaux x g k 1) = SNoCut (⋃_{k ∈ ω}SNo_sqrtaux x h k 0) (⋃_{k ∈ ω}SNo_sqrtaux x h k 1).

Use f_equal.

Apply famunion_ext to the current goal.

Let k be given.

Assume Hk.

We will prove SNo_sqrtaux x g k 0 = SNo_sqrtaux x h k 0.

Use f_equal.

Apply SNo_sqrtaux_ext x Hx g h to the current goal.

We will prove ∀w ∈ SNoS_ (SNoLev x), g w = h w.

An exact proof term for the current goal is Hgh.

An exact proof term for the current goal is omega_nat_p k Hk.

Apply famunion_ext to the current goal.

Let k be given.

Assume Hk.

We will prove SNo_sqrtaux x g k 1 = SNo_sqrtaux x h k 1.

Use f_equal.

Apply SNo_sqrtaux_ext x Hx g h to the current goal.

We will prove ∀w ∈ SNoS_ (SNoLev x), g w = h w.

An exact proof term for the current goal is Hgh.

An exact proof term for the current goal is omega_nat_p k Hk.

∎