Let x0 of type ι be given.
Apply unknownprop_e9c4cec7fb327dcb17b88acdaf76daee024e49fa71834a13065f86e12e958609 with
x0,
1,
λ x1 x2 . x2 = mul_nat x0 x0 leaving 2 subgoals.
The subproof is completed by applying nat_1.
Apply unknownprop_5858d8b36c7cdaccd2f26eae0cf9cb2cc1dc7fc685e15eee42b07d14732d6e73 with
x0,
λ x1 x2 . mul_nat x0 x2 = mul_nat x0 x0.
Let x2 of type ι → ι → ο be given.
Assume H0: x2 y1 y1.
The subproof is completed by applying H0.