Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply mul_SNo_com with
x0,
x2,
λ x3 x4 . SNoLt x4 (mul_SNo x1 x2) ⟶ SNoLt x0 x1 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H2.
Apply mul_SNo_com with
x1,
x2,
λ x3 x4 . SNoLt (mul_SNo x2 x0) x4 ⟶ SNoLt x0 x1 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
Apply unknownprop_a3252d6ac8fc90b05cfbead1aa6db1cdfa8cd486ea70700205ca3a4e7a90edc3 with
x2,
x0,
x1 leaving 4 subgoals.
The subproof is completed by applying H2.
The subproof is completed by applying H3.
The subproof is completed by applying H0.
The subproof is completed by applying H1.