Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
2,
3,
λ x0 x1 . x1 = 16 leaving 2 subgoals.
The subproof is completed by applying unknownprop_c6a33804dbf87f8ed348b0c7aa5a01ca7ba7d01ac6763a60fcde40c1affde745.
Apply unknownprop_4cbb45acbeb4637aed1f633ac0f8e87ad5c43bb92b99a6e174e317966d8c8d5e with
λ x0 x1 . mul_nat 2 x1 = 16.
Apply unknownprop_2bfb1c3614ff600c3c9dc68a9a9058028448f7c810281905f0eb1144a576489a with
8,
λ x0 x1 . x1 = 16 leaving 2 subgoals.
Apply unknownprop_1a52e19bf4045e8e446a298da7dba8c076ee67253cdcf7b15e893847906b7879 with
0.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_cb22f23c255b11e2fef1f0187745d1c6297e541a75b408830b470617abac132a with
8,
0,
λ x0 x1 . x1 = 16 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_bad5adbbba30ab6e9c584ed350d824b3c3bff74e61c0a5380ac75f32855c37ee with
8,
λ x0 x1 . ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc (ordsucc x1))))))) = 16.
Let x0 of type ι → ι → ο be given.
Assume H0: x0 16 16.
The subproof is completed by applying H0.