ABSTRACT. We address the problem of verifying the satisfiability of Constrained Horn Clauses (CHCs) based on theories of inductively defined data structures, such as lists or trees. We propose a transformation technique, related to Wadler's {\em deforestation}, whose objective is the removal of these data structures from the clauses, hence reducing their satisfiability to an equivalent satisfiability problem for CHCs on integers or booleans. We propose a basic transformation algorithm and identify a class of CHCs where it always succeeds. We also consider extensions of the basic algorithm which combine CHC transformation with reasoning on integer constraints, thus enlarging the class of CHCs where inductively defined data structures can be removed. We perform an experimental evaluation of our technique by considering a benchmark of verification problems for first order OCaml programs that process lists and trees. We show that our transformation greatly improves the effectiveness of applying the Z3 solver for CHCs. Our experiments also show that the verification technique based on CHC transformation followed by CHC solving, is competitive with respect to CHC solvers extended with induction.