Let x0 of type ι be given.
Apply unknownprop_a3a7565e6ec36921ef8d95ac6064e5fb0324fd3fb8dbfeef6aeadeb5800cae4a with
λ x1 x2 : ι → ο . x2 x0 ⟶ In 0 (ordsucc x0).
Assume H0:
(λ x1 . ∀ x2 : ι → ο . x2 0 ⟶ (∀ x3 . x2 x3 ⟶ x2 (ordsucc x3)) ⟶ x2 x1) x0.
Apply H0 with
λ x1 . In 0 (ordsucc x1) leaving 2 subgoals.
The subproof is completed by applying unknownprop_b28daf094ddd549776d741eec1dac894d28f0f162bae7bdbdbfb7366b31cdef0.
Let x1 of type ι be given.
Apply unknownprop_9d1f2833af10907d78259d2045ff2d1e1026643f459cca4199c4ae7f89385ba4 with
ordsucc x1,
0.
The subproof is completed by applying H1.