The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

To all,

If you're interested in a way to get full erasability in Coq, or yet 
another encoding of Red/Black trees in Coq, have a look at:

https://github.com/jonleivent/mindless-coding

Erasability is accomplished by adding a single injectivity axiom to a 
single wrapper Prop type (Erasable).  The readme explains things, and 
the Coq file is fairly well commented.

Any comments and/or criticisms are welcome!

-- Jonathan