Had a useful idea about this encoding while lying (laying? I can never remember.) in bed. I think I can throw this whole business of a limit predicate on terms out the window and just make the type-level definition
%abbrev lim = [n':nat] {n:nat} {y:phd} ({cvt:phd->hd} token n (cvt y)) -> ge n n' -> hd
and talk about terms at type lim n' for n' cranking down inductively as one chews through S while showing M . S = M' . S implies M = M'. Yeah, I think that should work.