An exact proof term for the current goal is CD_minus_add {2} SNo complex_tag_fresh minus_SNo add_SNo SNo_minus_SNo SNo_add_SNo minus_add_SNo_distr.