The Coq mailing list

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

I just discovered the ssreflect mailing list, so please ignore my question.

On Sat, Apr 14, 2012 at 9:51 AM, Andrej Bauer 
<andrej.bauer AT andrej.com>
 wrote:
> 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