Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
2,
2,
λ x0 x1 . x1 = 8 leaving 2 subgoals.
The subproof is completed by applying unknownprop_d97d6922f54612bc34684069408098060ad6c1b04a8b4fda7efccfad8c5e25b7.
Apply unknownprop_5c1c6be0c3ef8750ee14d5c0e6b369980cab68b09d15e01bcf36f823e05627e4 with
λ x0 x1 . mul_nat 2 x1 = 8.
Apply unknownprop_2bfb1c3614ff600c3c9dc68a9a9058028448f7c810281905f0eb1144a576489a with
4,
λ x0 x1 . x1 = 8 leaving 2 subgoals.
Apply unknownprop_5e2628df9f5f85e18b5435fd3c0ad09162064b9312de3fdc10d248bc12486c0b with
0.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_ae47a38e201daae59edf8724f290c3473f31a249345a4fe6f394ae507b501f4b with
4,
0,
λ x0 x1 . x1 = 8 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_bad5adbbba30ab6e9c584ed350d824b3c3bff74e61c0a5380ac75f32855c37ee with
4,
λ x0 x1 . ordsucc (ordsucc (ordsucc (ordsucc x1))) = 8.
Let x0 of type ι → ι → ο be given.
Assume H0: x0 8 8.
The subproof is completed by applying H0.