An exact proof term for the current goal is CD_add_proj1 {2} SNo complex_tag_fresh add_SNo SNo_add_SNo.