Implementing map for trees in agda - termination checking problem

Question

I'm trying to implement Trees in agda as follows:

module Tree where

open import Data.List

data Tree (A : Set) : Set where
  node : List (Tree A) → Tree A
  leaf : A → Tree A

{-
The straightforward solution upsets the termination checker:
mapTree : ∀ {A B} → (A → B) → Tree A → Tree B
mapTree f (node ts) = node (map (mapTree f) ts)
mapTree f (leaf x) = leaf (f x)
-}

Since the call to mapTree f is not structural recursive, this code is not allowed by the termination checker. So I have to resort to a mutual recursion:

mapTree : ∀ {A B} → (A → B) → Tree A → Tree B
mapTree' : ∀ {A B} → (A → B) → List (Tree A) → List (Tree B)

mapTree f (node ts) = node (mapTree' f ts)
mapTree f (leaf x) = leaf (f x)

mapTree' f [] = []
mapTree' f (t ∷ ts) = mapTree f t ∷ mapTree' f ts

The problem is that this is an unnecessary repetition and specialization of a library function map, and requires knowledge of the internal workings of Lists (imagine if one decides to switch to ℕ → A later).

How is this problem usually dealt with? More generally, is there some sort of tricks/idioms to keep the termination checker happy without breaking layers of abstraction and encapsulation?