Comment by gelisam

The [Beluga language](http://complogic.cs.mcgill.ca/beluga/) is a variant of Twelf which aims to make such transformations much easier.

Full disclosure: Brigitte Pientka was my supervisor. I did not work on the compiler, but I did make the language's logo.