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