[Agda] mutual recursion

[Dan Licata]

Agda allows the definition of mutually recursive functions, where one
appears in the type of the other.  E.g. if

  Tp : Set
  Tm : Tp -> Set

then we can define

  mutual
    tpsem : Tp -> Set
    tpsem = {!!} 
  
    tmsem : {A : Tp} -> Tm A -> tpsem A
    tmsem = {!!}

Is there a good description somewhere of how these definitions be
reduced to ones that don't use this feature?

-Dan