The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

I am looking at ssreflect, which I think is very nice. When it comes
to rewriting there is special treatment of eq. Does ssreflect also
work with eq-in-type, i.e., the inductively defined type identity
which is like eq but maps into Type? Would it be complicated to
support it?

With kind regards,

Andrej