I love it! Great job.
This is a nice discovery.
Have you seen this? Termination checking for type substitution It’s closer to your example in that it encodes a possibly non-terminating computation, rather than an undecidable question per se.
(Also here’s a well-actually: my post from 2020 that you linked technically doesn’t prove Turing-completeness. Nowadays protocols with undecidable word problems (and some with decidable too or course) are rejected during type checking because completion fails, and once completion succeeds we can solve word problems by computing normal forms, which always terminates)