Let x0 of type ι be given.
Apply unknownprop_0a5886fc885b1c9f8fc11c33cf1490ed0f895fb191d89ada0539224964f60b42 with
λ x1 x2 : ι → ι → ι . x2 x0 0 = x0.
The subproof is completed by applying unknownprop_18742339ed2086348f526a0d540f93b8d9ad1499a803d12adbb11e4be06bf7bb with
x0,
λ x1 x2 . ordsucc x2.