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