What about mutual recursion?

• Mutually recursive functions give rise to
  1. simultaneously defined inductive domain predicates,
  2. mutually recursive translated functions.
• No problem!