Let x0 of type ι be given.
Let x1 of type ι be given.
Apply CSNo_add_CSNo with
x0,
x1 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply unknownprop_06a4ec1d06df31c2c8c53ecdf2780bb9f187c1468b28741ccdfd338035b0de7f with
add_CSNo x0 x1,
minus_CSNo (add_CSNo x0 x1),
add_CSNo (minus_CSNo x0) (minus_CSNo x1) leaving 4 subgoals.
The subproof is completed by applying L2.
Apply CSNo_minus_CSNo with
add_CSNo x0 x1.
The subproof is completed by applying L2.
Apply CSNo_add_CSNo with
minus_CSNo x0,
minus_CSNo x1 leaving 2 subgoals.
Apply CSNo_minus_CSNo with
x0.
The subproof is completed by applying H0.
Apply CSNo_minus_CSNo with
x1.
The subproof is completed by applying H1.
Apply add_CSNo_minus_CSNo_rinv with
add_CSNo x0 x1,
λ x2 x3 . x3 = add_CSNo (add_CSNo x0 x1) (add_CSNo (minus_CSNo x0) (minus_CSNo x1)) leaving 2 subgoals.
The subproof is completed by applying L2.
Apply unknownprop_bc5d75aef1cebf250904193b318ff14152dec1ee6de37ede33809ace5bf4802f with
x0,
x1,
minus_CSNo x0,
minus_CSNo x1,
λ x2 x3 . 0 = x3 leaving 5 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Apply CSNo_minus_CSNo with
x0.
The subproof is completed by applying H0.
Apply CSNo_minus_CSNo with
x1.
The subproof is completed by applying H1.
Apply add_CSNo_minus_CSNo_rinv with
x0,
λ x2 x3 . 0 = add_CSNo x3 (add_CSNo x1 (minus_CSNo x1)) leaving 2 subgoals.
The subproof is completed by applying H0.
Apply add_CSNo_minus_CSNo_rinv with
x1,
λ x2 x3 . 0 = add_CSNo 0 x3 leaving 2 subgoals.
The subproof is completed by applying H1.
Apply add_CSNo_0L with
0,
λ x2 x3 . 0 = x3 leaving 2 subgoals.
The subproof is completed by applying unknownprop_85a866d410bbf26b260c37246259122da00d151df84a9a2a98da7e65f3fcf36a.
Let x2 of type ι → ι → ο be given.
Assume H3: x2 0 0.
The subproof is completed by applying H3.