  It is known that the verification of imperative, functional, and logic
programs can be reduced to the satisfiability of constrained Horn clauses
(CHCs), and this satisfiability check can be performed by using CHC solvers,
such as Eldarica and Z3. These solvers perform well when they act on simple
constraint theories, such as Linear Integer Arithmetic and the theory of
Booleans, but their efficacy is very much reduced when the clauses refer to
constraints on inductively defined structures, such as lists or trees.
Recently, we have presented a transformation technique for eliminating those
inductively defined data structures, and hence avoiding the need for
incorporating induction principles into CHC solvers. However, this technique
may fail when the transformation requires the use of lemmata whose generation
needs ingenuity. In this paper we show, through an example, how during the
process of transforming CHCs for eliminating inductively defined structures one
can introduce suitable predicates, called difference predicates, whose
definitions correspond to the lemmata to be introduced. Through a second
example, we show that, whenever difference predicates cannot be introduced, we
can introduce, instead, auxiliary queries which also correspond to lemmata, and
the proof of these lemmata can be done by showing the satisfiability of those
queries.
