Can all regular tree types be expressed as $\mu$ types?

In "Types and Programming Languages", Pierce gives a translation from recursive types ($$\mu$$ types) to types expressed as regular trees: possibly infinite trees, but with finitely many distinct subtrees.

I'm wondering, is the converse true? Can every regular tree type be expressed using the $$\mu$$ fixpoint notation? It seems obvious that this can be done if you have mutually recursive types: you have a type for each subtree of the regular tree type. But can it be done with singly recursive types?

• You can reduce mutable recursion to a single recursion, see Bekic's Theorem, see e.g. Section 10.1 of Winskel's book The Formal Semantics of Programming Languages. – Martin Berger May 22 at 21:54
• @MartinBerger Perfect, just what I was looking for! – jmite May 23 at 0:55
• @MartinBerger If you write that as an answer I'll accept it – jmite May 23 at 0:55