Let x0 of type ι be given.
Let x1 of type ι be given.
Apply CSNo_ReIm_split with
add_CSNo x0 x1,
add_CSNo x1 x0 leaving 4 subgoals.
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 CSNo_add_CSNo with
x1,
x0 leaving 2 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
Let x3 of type ι → ο be given.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
x1,
y2,
λ x4 . x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x5 of type ι → ο be given.
Apply add_SNo_com with
CSNo_Re y2,
CSNo_Re x3,
λ x6 . x5 leaving 3 subgoals.
Apply CSNo_ReR with
y2.
The subproof is completed by applying H0.
Apply CSNo_ReR with
x3.
The subproof is completed by applying H1.
Apply unknownprop_af0b151803c2dc4bc6691b166645c0a8471b89f2da30fa0948427517708d6da0 with
x3,
y2,
λ x6 x7 . (λ x8 . x5) x7 x6 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
set y5 to be λ x5 . y4
Apply L3 with
λ x6 . y5 x6 y4 ⟶ y5 y4 x6 leaving 2 subgoals.
Assume H4: y5 y4 y4.
The subproof is completed by applying H4.
The subproof is completed by applying L3.
Let x3 of type ι → ι → ο be given.
Apply L2 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H3: x3 y2 y2.
The subproof is completed by applying H3.
Let x3 of type ι → ο be given.
Apply unknownprop_7f97cbea1b316ccd537155d989f2889dd5c3074e8edefbeca1dbc06c62876158 with
x1,
y2,
λ x4 . x3 leaving 3 subgoals.
The subproof is completed by applying H0.
The subproof is completed by applying H1.
Let x5 of type ι → ο be given.
Apply add_SNo_com with
CSNo_Im y2,
CSNo_Im x3,
λ x6 . x5 leaving 3 subgoals.
Apply CSNo_ImR with
y2.
The subproof is completed by applying H0.
Apply CSNo_ImR with
x3.
The subproof is completed by applying H1.
Apply unknownprop_7f97cbea1b316ccd537155d989f2889dd5c3074e8edefbeca1dbc06c62876158 with
x3,
y2,
λ x6 x7 . (λ x8 . x5) x7 x6 leaving 3 subgoals.
The subproof is completed by applying H1.
The subproof is completed by applying H0.
The subproof is completed by applying H3.
set y5 to be λ x5 . y4
Apply L3 with
λ x6 . y5 x6 y4 ⟶ y5 y4 x6 leaving 2 subgoals.
Assume H4: y5 y4 y4.
The subproof is completed by applying H4.
The subproof is completed by applying L3.
Let x3 of type ι → ι → ο be given.
Apply L2 with
λ x4 . x3 x4 y2 ⟶ x3 y2 x4.
Assume H3: x3 y2 y2.
The subproof is completed by applying H3.