An exact proof term for the current goal is OSNo_proj0_2 0 1 HSNo_0 HSNo_1.