An exact proof term for the current goal is CD_add_mul_distrR {3} CSNo quaternion_tag_fresh minus_CSNo conj_CSNo add_CSNo mul_CSNo CSNo_minus_CSNo CSNo_conj_CSNo CSNo_add_CSNo CSNo_mul_CSNo minus_add_CSNo add_CSNo_assoc add_CSNo_com mul_CSNo_distrL mul_CSNo_distrR.