An exact proof term for the current goal is CD_add_minus_linv {2} SNo complex_tag_fresh minus_SNo add_SNo SNo_minus_SNo add_SNo_minus_SNo_linv.