rewrite the current goal using conj_OSNo_conj_HSNo 1 HSNo_1 (from left to right).

An exact proof term for the current goal is conj_HSNo_1.

∎