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