Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Let x3 of type ι be given.
Apply unknownprop_01b7f7993ff222473c0dc551f861729864a2fa847d49dc4751edad0602198144 with
setprod x2 x3,
setprod x0 x1,
mul_nat x0 x1 leaving 2 subgoals.
Apply unknownprop_4eb79cb3f631e5466c7788d716ccb7e1b7deb9acee65e574ff006d427d7f78a0 with
x2,
x3,
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
Apply unknownprop_a74a58443988b06ca5d135cd640cf27ee2c3cca704636becdd1a899811175a3a with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.