Let α and β be given.

Assume Ha Hb Hab.

Let x be given.

Assume Hx: x ∈ SNoS_ α.

Apply SNoS_E α Ha x Hx to the current goal.

Let γ be given.

Assume Hc.

Apply Hc to the current goal.

Assume Hc1: γ ∈ α.

Assume Hc2: SNo_ γ x.

An exact proof term for the current goal is SNoS_I β Hb x γ (Hab γ Hc1) Hc2.

∎