The main result is a proof method for verification conditions arising from a program annotated with assertions. The method has two main components. First and foremost is an unfolding algorithm which works by reducing the recursive definitions so that a constraint proof may now be applied. Here we introduce a notion of {\em coinduction} which forms the basis for termination of the unfolding process. The second step is to reduce the constraints, which in general contain expressions involving all the three data types of integers, arrays and multisets, into a base constraint involving only integer constraints. Base constraints can then be dispensed with available solvers.
We finally show via a small benchmark of classic examples that our proof method is practical.