Let x0 of type ι be given.
Apply Eps_i_ex with
λ x1 . and (SNo x1) (∃ x2 . and (SNo x2) (∃ x3 . and (SNo x3) (∃ x4 . and (SNo x4) (∃ x5 . and (SNo x5) (∃ x6 . and (SNo x6) (∃ x7 . and (SNo x7) (∃ x8 . and (SNo x8) (x0 = bbc71.. x1 x2 x3 x4 x5 x6 x7 x8)))))))).
The subproof is completed by applying H0.