Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_0a5886fc885b1c9f8fc11c33cf1490ed0f895fb191d89ada0539224964f60b42 with
λ x2 x3 : ι → ι → ι . x3 x0 (ordsucc x1) = ordsucc (x3 x0 x1).
Apply unknownprop_4e3b33b1166f6152a39a44a865c600b0b9f1dfa87f521be03670a83f1d10a167 with
x0,
λ x2 x3 . ordsucc x3,
x1.
The subproof is completed by applying H0.