Apply CD_add_assoc {4} HSNo octonion_tag_fresh add_HSNo HSNo_add_HSNo add_HSNo_assoc to the current goal.