Let alpha and beta be given.

Assume Ha Hb Hab.

Let x be given.

Assume Hx: x ∈ SNoS_ alpha.

Apply SNoS_E alpha Ha x Hx to the current goal.

Let gamma be given.

Assume Hc.

Apply Hc to the current goal.

Assume Hc1: gamma ∈ alpha.

Assume Hc2: SNo_ gamma x.

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

∎