We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on Constrained Horn Clauses (CHCs) by which the verification problem is reduced to the problem of checking satisfiability of a set of clauses derived from the given program and contracts. We consider programs that manipulate Algebraic Data Types (ADTs) and a class of contracts specified by using catamorphisms, that is, functions defined by a simple recursion schema on the given ADT. We show by several examples that state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problems obtained by direct translation of the contracts into CHCs. Then, we propose a transformation technique that removes the ADT terms from CHCs, thereby deriving new sets of clauses that work on basic sorts, such as integers and booleans. We prove that the transformation is sound, in the sense that if the transformed set of CHCs is satisfiable, then so is the original set. We also prove that the transformation always terminates for the class of contracts specified by catamorphisms. Finally, we present the experimental results obtained by an implementation of our technique when verifying many non-trivial contracts relative to list sorting and tree manipulating programs.