[tel]

It can be kind of hard to satisfy termination checkers, though. They're not smart. You basically have to show structural induction on something which sometimes forces you to invent lots of new proof terms.

[Ono-Sendai]

Indeed. I suspect that's where a lot of my time will be invested, making the checker better, improving error messages, etc..