How difficult would it be to write a Coq plugin to perform these translations? The thing I like about Coq is that it appears to have better tooling than the ot

How difficult would it be to write a Coq plugin to perform these translations? The thing I like about Coq is that it appears to have better tooling than the other theorem provers (coqtop, proof-general for emacs), and you can extract code for other programming languages. I haven't looked in great detail at the alternatives though.