Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_ca08d837d9b021979c5586a33301880578d4443dca4b10b9b2f206cbc9855b95 with
x1,
λ x2 x3 . equip x2 (mul_nat x0 x0).
Apply unknownprop_b8fbbba1527cbd64146da68212d93c3041b26e632212bb254ebdd564a5aa3700 with
x0,
x0,
x1,
x1 leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
The subproof is completed by applying H1.