Proofgold Proof

pf
Apply CD_add_0L 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_0L. ■