Proofgold Proof

pf
Apply CD_add_0R with Sing 2, SNo, add_SNo leaving 3 subgoals. The subproof is completed by applying complex_tag_fresh. The subproof is completed by applying SNo_0. The subproof is completed by applying add_SNo_0R. ■