List of improvements to make for the Coq plugin: - [ ] make the catt implicit arguments implicit in coq as well - [ ] after #62 formal substitutions are added: add declaration of terms in coq and use them as variables instead of inlining everything
List of improvements to make for the Coq plugin: