Thanks Henning, and apologies for the delay in replying.
I more had in mind your `n + 'Zero -> n` example. With cunning overlaps you can also achieve `'Zero + n -> n`; and even from result 'Zero improve both arguments to 'Zero.
With class ForthBack, a FunDep right-to-left would (maybe) expand `a` to `Forth (Back a)` -- which hardly seems helpful and is anyway not true: `Forth (Forth (Back (Back a)))` would be just as legit.
That kind of recursion-depth-sensitive normalisation is possible with FunDeps and overlaps. But I'd need to recharge my Oleg batteries.