Apply CD_conj_invol with
Sing 2,
SNo,
minus_SNo,
λ x0 . x0 leaving 5 subgoals.
The subproof is completed by applying complex_tag_fresh.
The subproof is completed by applying SNo_minus_SNo.
Let x0 of type ι be given.
The subproof is completed by applying H0.
The subproof is completed by applying minus_SNo_invol.
Let x0 of type ι be given.
Let x1 of type ι → ι → ο be given.
Assume H1: x1 x0 x0.
The subproof is completed by applying H1.