An exact proof term for the current goal is HSNo_proj0_2 0 i CSNo_0 CSNo_Complex_i.