Comment by zozbot234

Very nice work. This kind of embedding (a direct equivalent to "transpiling" for code) is quite common in the formal methods community; for example, Freek Wiedijk has shown a similar embedding of HOL Light https://www.cs.ru.nl/~freek/notes/index.html into Coq.