Let x0 of type ι be given.
Apply H0 with
λ x1 x2 . ∀ x3 . x3 ∈ x2 ⟶ ∀ x4 : ο . (∀ x5 . x5 ∈ omega ⟶ ∀ x6 . x6 ∈ ap x0 x5 ⟶ x3 = lam 2 (λ x7 . If_i (x7 = 0) x5 x6) ⟶ x4) ⟶ x4.
The subproof is completed by applying unknownprop_7e890e3c212f35a253b09f8bdf3ce512e10f8816e882a3da817fe1bc10582407 with
omega,
λ x1 . ap x0 x1.