Let x0 of type ι be given.
Let x1 of type ι be given.
Let x2 of type ι be given.
Apply CSNo_ReIm_split with
add_CSNo x0 (add_CSNo x1 x2),
add_CSNo (add_CSNo x0 x1) x2 leaving 4 subgoals.
Apply CSNo_add_CSNo with
x0,
add_CSNo x1 x2 leaving 2 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
Apply CSNo_add_CSNo with
add_CSNo x0 x1,
x2 leaving 2 subgoals.
The subproof is completed by applying L4.
The subproof is completed by applying H2.
set y3 to be ...
Let x4 of type ι → ο be given.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
x1,
add_CSNo x2 y3,
λ x5 . x4 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying L3.
set y5 to be ...
Let x6 of type ι → ο be given.
set y7 to be ...
Let x8 of type ι → ο be given.
Apply f_eq_i with
λ x9 . add_SNo (CSNo_Re y3) x9,
CSNo_Re (add_CSNo x4 y5),
add_SNo (CSNo_Re x4) (CSNo_Re y5),
λ x9 . x8 leaving 2 subgoals.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
x4,
y5 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H2.
set y9 to be ...
Let x10 of type ι → ο be given.
Apply add_SNo_assoc with
CSNo_Re x4,
CSNo_Re y5,
CSNo_Re x6,
λ x11 . x10 leaving 4 subgoals.
Apply CSNo_ReR with
x4.
The subproof is completed by applying H0.
Apply CSNo_ReR with
y5.
The subproof is completed by applying H1.
Apply CSNo_ReR with
x6.
The subproof is completed by applying H2.
set y11 to be ...
Let x12 of type ι → ο be given.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
y5,
x6,
λ x13 x14 . (λ x15 . x12) ((λ x15 . add_SNo x15 (CSNo_Re y7)) x13) ((λ x15 . add_SNo x15 ...) ...) leaving 2 subgoals.
set y12 to be λ x12 x13 . (λ x14 . y11) x13 x12
Apply L9 with
λ x13 . y12 x13 y11 ⟶ y12 y11 x13 leaving 2 subgoals.
Assume H10: y12 y11 y11.
The subproof is completed by applying H10.
The subproof is completed by applying L9.
set y10 to be λ x10 . y9
Apply L8 with
λ x11 . y10 x11 y9 ⟶ y10 y9 x11 leaving 2 subgoals.
Assume H9: y10 y9 y9.
The subproof is completed by applying H9.
The subproof is completed by applying L8.
set y8 to be λ x8 . y7
Apply L7 with
λ x9 . y8 x9 y7 ⟶ y8 y7 x9 leaving 2 subgoals.
Assume H8: y8 y7 y7.
The subproof is completed by applying H8.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
add_CSNo x4 y5,
x6,
λ x9 x10 . (λ x11 . y8) x10 x9 leaving 3 subgoals.
The subproof is completed by applying H5.
The subproof is completed by applying L3.
The subproof is completed by applying L7.
set y6 to be λ x6 . y5
Apply L6 with
λ x7 . y6 x7 y5 ⟶ y6 y5 x7 leaving 2 subgoals.
Assume H7: y6 y5 y5.
The subproof is completed by applying H7.
The subproof is completed by applying L6.
Let x4 of type ι → ι → ο be given.
Apply L5 with
λ x5 . x4 x5 y3 ⟶ x4 y3 x5.
Assume H6: x4 y3 y3.
The subproof is completed by applying H6.