Let x0 of type ι be given.
Apply CSNo_ReR with
x0.
The subproof is completed by applying H0.
Apply CSNo_ImR with
x0.
The subproof is completed by applying H0.
Apply SNo_add_SNo with
exp_SNo_nat (CSNo_Re x0) 2,
exp_SNo_nat (CSNo_Im x0) 2 leaving 2 subgoals.
Apply SNo_exp_SNo_nat with
CSNo_Re x0,
2 leaving 2 subgoals.
The subproof is completed by applying L1.
The subproof is completed by applying nat_2.
Apply SNo_exp_SNo_nat with
CSNo_Im x0,
2 leaving 2 subgoals.
The subproof is completed by applying L2.
The subproof is completed by applying nat_2.