Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_2a206e952ad25cce114176c1bd00b9616616e077a487ae57de9a81a2597e9fbb with
mul_SNo x0 x1.
Apply unknownprop_2aab862768903d1c5aee7f2f0ed0632273e38b62a9c448fbe58583ccfcf9092d with
x0,
x1 leaving 2 subgoals.
Apply unknownprop_ffb5b84d40e47086b40f6e4db6ec10ef78d20da64c3abaac23ff2569830b3d1c with
x0.
The subproof is completed by applying H0.
Apply unknownprop_ffb5b84d40e47086b40f6e4db6ec10ef78d20da64c3abaac23ff2569830b3d1c with
x1.
The subproof is completed by applying H1.