Let z, w and v be given.
Assume Hz Hw Hv.
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
Apply CSNo_add_CSNo to the current goal.
An exact proof term for the current goal is ??.
An exact proof term for the current goal is ??.
∎