For what it's worth, Emacs already does that last thing. As a contrived example borrowed from a post I wrote a while back[1]:

    \ a b c -> a >= b && b <= c || a /= c

gets rendered as:

    λ a b c → a ≥ b ∧ b ≤ c ∨ a ≢ c

However, this is a bit of a pain to do in general. It works well for common functions and syntax elements, but has to be built into the editor. Doing it more generally would require the author of the initial function to come up with multiple different names for it, which sounds unlikely.

[1]: https://news.ycombinator.com/item?id=4742616