Conditional literals are expressive constructs for knowledge representation supported by clingo, whose semantics can be character- ized in terms of a translation into second-order logic. Here we compare two perspectives on the semantics of conditional literals by defining a theoretical language of logic programs with arithmetic and conditional literals of two kinds. Then we adapt results on the strong equivalence of programs with arithmetic to our considered language. This enables us to automate strong equivalence verification of such programs with an extension of the anthem proof assistant. Finally, we investigate some common syntactic conditions under which the semantics of both kinds of conditional literals coincide.