Let x0 of type ι be given.
Apply unknownprop_f23dde3020cfe827bdc4db0338b279dd2c0f6c90742a195a1a7a614475669076 with
λ x1 . nat_p (mul_nat x0 x1) leaving 2 subgoals.
Apply unknownprop_4756ca8c34efd0461ee4f316febaf4ee77ac8f03a3f9f75c481b60c5f8500b17 with
x0,
λ x1 x2 . nat_p x2.
The subproof is completed by applying unknownprop_0e150139fedb8d7a0ae85e3054b4c73c936e7acb880ce730fb00a0093c9c6c27.
Let x1 of type ι be given.
Apply unknownprop_3defe724d02ba276d9730f9f5a87e86e6bc0e48da350a99bdaaf13f339867dcf with
x0,
x1,
λ x2 x3 . nat_p x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply unknownprop_3336121954edce0fefb5edee2ad1b426a9827aac09625122db0ff807b493dc73 with
x0,
mul_nat x0 x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.