Let x0 of type ι be given.

Assume H0: ordinal x0.

Let x1 of type ι be given.

Assume H1: SNo_ x0 x1.

Apply unknownprop_7e7a3c7a04dac475d679ef0eb25eb83b9a217d071452ad37861b7c785c606e42 with λ x2 x3 : ι → ο . x3 x1.

Let x2 of type ο be given.

Assume H2: ∀ x3 . and (ordinal x3) (SNo_ x3 x1) ⟶ x2.

Apply H2 with x0.

Apply unknownprop_389e2fb1855352fcc964ea44fe6723d7a1c2d512f04685300e3e97621725b977 with ordinal x0, SNo_ x0 x1 leaving 2 subgoals.

The subproof is completed by applying H0.

The subproof is completed by applying H1.

■

Proofgold Proof