Proofgold Proof

pf
Apply CD_conj_proj1 with Sing 2, SNo, minus_SNo, λ x0 . x0 leaving 3 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. Assume H0: SNo x0. The subproof is completed by applying H0. ■