Contractiveness not required for regularity

Yesterday I wrote about ensuring termination of subtyping for equirecursive types that I thought contractiveness ensures that the (potentially) infinite tree corresponding to a recursive type is regular. That was wrong. Contractiveness just ensures that you can't represent types that don't have a corresponding tree, such as μA.A. The fact that the tree is regular comes from the fact that the syntactic representation is finite and substitution doesn't add anything new.