I had/have a similar feeling. I have thought about it some time ago and came up with the following proposal: http://matej-kosik.github.io/www/doc/coq/coq-trun

I had/have a similar feeling. I have thought about it some time ago and came up with the following proposal: http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tree/index.html http://matej-kosik.github.io/www/doc/coq/coq-trunk-proof-tre...