Let x be given.

Assume Hx.

rewrite the current goal using conj_HSNo_conj_CSNo x (SNo_CSNo x Hx) (from left to right).

We will prove x ' = x.

An exact proof term for the current goal is conj_CSNo_id_SNo x Hx.

∎