Let x0 of type ι be given.
Apply unknownprop_adc51df32e37a02ae01a7627d71f293cbf548824fcf0d70ccbf318430642e27c with
x0,
0,
λ x1 x2 . x2 = x0 leaving 2 subgoals.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Apply unknownprop_4ef67fc5b8b30ebc0b691020299a978fd97f9ab288d7f37b768f51bf86e2a3c3 with
x0,
λ x1 x2 . mul_nat x0 x2 = x0.
The subproof is completed by applying unknownprop_74e06c9344760e4cc873ef5c22b83470d591f1b41a22d02c74881e98d2f21e46 with x0.