Let x0 of type ι be given.
Let x1 of type ι be given.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with
x0,
minus_CSNo x1,
λ x2 x3 . x3 = minus_CSNo (mul_CSNo x0 x1) leaving 3 subgoals.
The subproof is completed by applying H0.
Apply CSNo_minus_CSNo with
x1.
The subproof is completed by applying H1.
Apply unknownprop_78927d114a9e016b6fa814cd3cb647b02601a2956c15aa990b929c9491fbf104 with
x1,
x0,
λ x2 x3 . x3 = minus_CSNo (mul_CSNo x0 x1) leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Apply unknownprop_4be0565ac5b41f138f7a30d0a9f34a5d126bb341d2eeaa545aa7f0c1552b9722 with
x0,
x1,
λ x2 x3 . minus_CSNo (mul_CSNo x1 x0) = minus_CSNo x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x3 of type ι → ι → ο be given.
Assume H2: x3 y2 y2.
The subproof is completed by applying H2.