Let x0 of type ι be given.
Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with
λ x1 . nat_p (69aae.. x0 x1) leaving 2 subgoals.
Apply unknownprop_4ef67fc5b8b30ebc0b691020299a978fd97f9ab288d7f37b768f51bf86e2a3c3 with
x0,
λ x1 x2 . nat_p x2.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
Let x1 of type ι be given.
Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
x0,
x1,
λ x2 x3 . nat_p x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_0b229518762ed7010020950c24a2d0fe47c44c7a7b255cdddc862baf12395763 with
x0,
69aae.. x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.