An exact proof term for the current goal is CD_minus_F_eq {4} HSNo octonion_tag_fresh minus_HSNo HSNo_0 minus_HSNo_0.