The Coq mailing list

[see tolearn <seetolearn AT mail.ru>]

Consider theorem 'prop_eq':
> Definition prop_eq := fun p q (eq1:p=q)
        => (match eq1 in _=qdep return p->qdep
        with refl_equal => fun p=>p
        end) : p->q.

Then:
> Variable (x1 x2 y1 y2:nat) (eq1:x1=y1) (eq2:x2=y2) (lt1:x1<x2).
> Check prop_eq (x1 < x2) (y1 < y2) (f_equal2 lt eq1 eq2) lt1.
gives an error message:
{{{
Error: The term "f_equal2 lt eq1 eq2" has type "(x1 < x2) = (y1 < y2)"
 while it is expected to have type "(x1 < x2) = (y1 < y2)"
}}}
The terms actually are identic. Am I missing something? I'm
using CoqIde, coqtop version 8.1pl1 (Jul. 2007), Linux.

Best regards,
Roman Beslik.