Let x0 of type ι be given.
Apply unknownprop_3ecd982cbc53bc522aff3fa68eac8a88bfce787ef3776f0dfe2618ef278e2daf with
x0,
0 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
Apply unknownprop_28b7bd7c495fc6d6aba877cec7421acb6ac63eedc181bb03d3f51f298d7e9d45 with
mul_CSNo x0 0,
0,
mul_CSNo x0 0 leaving 4 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
The subproof is completed by applying L1.
Apply unknownprop_1a3b6d576749bdb66b853eab2e35cc4332be69b97fdfebcc7e17a4a552a3d204 with
x0,
0,
0,
λ x1 x2 . x1 = add_CSNo 0 (mul_CSNo x0 0) leaving 4 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
Apply add_CSNo_0L with
0,
λ x1 x2 . mul_CSNo x0 x2 = add_CSNo 0 (mul_CSNo x0 0) leaving 2 subgoals.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
Let x1 of type ι → ι → ο be given.
Apply add_CSNo_0L with
mul_CSNo x0 0,
λ x2 x3 . x1 x3 x2.
The subproof is completed by applying L1.