Proofgold Proof

pf
Let x0 of type ι be given. Let x1 of type ι be given. Assume H0: CSNo x0. Assume H1: CSNo x1. Assume H2: CSNo (add_CSNo x1 x0). Apply unknownprop_6df04587a59e9b54f0549c96144213d94328d0b365474f739b895e743839c817 with x0, x1 leaving 2 subgoals. The subproof is completed by applying H0. The subproof is completed by applying H1. ■