We will prove CSNo (pa 0 1).

Apply CSNo_I to the current goal.

An exact proof term for the current goal is SNo_0.

An exact proof term for the current goal is SNo_1.

∎