An exact proof term for the current goal is CD_exp_nat_S {2} SNo complex_tag_fresh minus_SNo conj add_SNo mul_SNo.