Termination-checking of function over a trie

问题:

I'm having difficulty convincing Agda to termination-check the function fmap below and similar functions defined recursively over the structure of a Trie. A Trie is a trie whose domain is a Type, an object-level type formed from unit, products and fixed points (I've omitted coproducts to keep the code minimal). The problem seems to relate to a type-level substitution I use in the definition of Trie. (The expression const (μₜ τ) * τ means apply the substitution const (μₜ τ) to the type τ.)

module Temp where

   open import Data.Unit
   open import Category.Functor
   open import Function
   open import Level
   open import Relation.Binary

   -- A context is just a snoc-list.
   data Cxt {