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