We prove the intermediate claim L1: ∀z, SNo z → ∀g h : set → set, (∀u ∈ SNoS_ (SNoLev z), g u = h u) → G w f z g = G w f z h.

Let z be given.

Assume Hz.

Let g and h be given.

Assume Hgh.

We prove the intermediate claim L1a: ∀x ∈ SNoS_ (SNoLev w), f x = f x.

Let x be given.

Assume Hx.

Use reflexivity.

An exact proof term for the current goal is SNo_rec2_G_prop w Hw f f L1a z Hz g h Hgh.

An exact proof term for the current goal is SNo_rec_i_eq (G w f) L1.