An exact proof term for the current goal is CD_conj_minus {2} SNo complex_tag_fresh minus_SNo conj SNo_minus_SNo (λx H ⇒ H) (λx _ q H ⇒ H).