It's a good thing there are Coq proofs. However, I would still like to see the paper though. A paper is supposed to be more than just a syntactic theory. Typically there is some motivation included as well.