This paper presents a fully automatic method for proving properties on polymorphic programs over algebraic data types. This method works by reducing the verification of such properties to the verification of properties on monomorphic programs over a finite domain. For programs without polymorphic equality, the reduction exploits Wadler’s “Theorem for Free”. For programs using polymorphic equality, we provide a sufficient condition for the reduction to hold. The condition relies on the existence of a locally complete abstraction function whose image is a finite set of arbitrary constants chosen for abstracting primitive values. The number of arbitrary constants depends on the functions under concern and the properties to prove. We present an implementation that automatically computes the number of constants and, thus, ensures that proving the polymorphic case with equality can be reduced to the proof carried out on a monomorphic instance of the program. Experimental results show that this reduction is indeed possible and can be done with a small number of constants. Target programs support user-defined recursive ADTs and recursive first-order functions.