Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply SNoR_E with
mul_SNo x0 x1,
x2,
or (∃ x3 . and (x3 ∈ SNoL x0) (∃ x4 . and (x4 ∈ SNoR x1) (SNoLe (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo x2 (mul_SNo x3 x4))))) (∃ x3 . and (x3 ∈ SNoR x0) (∃ x4 . and (x4 ∈ SNoL x1) (SNoLe (add_SNo (mul_SNo x3 x1) (mul_SNo x0 x4)) (add_SNo x2 (mul_SNo x3 x4))))) leaving 3 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying H4.
Apply L3 with
x2 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying H6.
The subproof is completed by applying H7.