Proofgold Proof

pf
Apply CD_minus_invol with Sing 2, SNo, minus_SNo leaving 3 subgoals. The subproof is completed by applying complex_tag_fresh. The subproof is completed by applying SNo_minus_SNo. The subproof is completed by applying minus_SNo_invol. ■