We discuss a programming exercise in which we have generalized Tim Sheard's generic unification algorithm (ICFP'01) to cope with mutually recursive term datatypes. The programming language of choice is Cayenne, where we use dependent types to encode records of types for the recursive parameter in the term datatypes.

Slides in compressed PostScript.