Let x0 of type ι be given.
Apply unknownprop_0c1ade26592410d89f01c361472f3ed43aba002bace9b64b2864e15aabc87412 with
λ x1 x2 . mul_nat x1 x0 = add_nat x0 x0.
Apply unknownprop_3cb222ff3c5eee07230d070fbc3f28a82ac82ef3a8a332432b591d09716abcbb with
1,
1,
x0,
λ x1 x2 . x2 = add_nat x0 x0 leaving 4 subgoals.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
The subproof is completed by applying unknownprop_8d353ccfb170ea018406af7266d499508cf5be2cebcac5c8a89ccd16a50d0251.
The subproof is completed by applying H0.
Apply unknownprop_3c96f64bbe53873aa75f0b891c83c659d16cbe53c811762d28a0df6657027827 with
x0,
λ x1 x2 . add_nat x2 x2 = add_nat x0 x0 leaving 2 subgoals.
The subproof is completed by applying H0.
Let x1 of type ι → ι → ο be given.
The subproof is completed by applying H1.