The Coq mailing list

[rabforum <rabforum AT ukr.net>]

Thanks for replies. I should have known about "Set Printing All" and 
@-notation.
I thought that definition assumes that (p q:Prop). In fact it may be (p 
q:Set).

> Now, running the [Check] command again, you get this more explicit message:
>     Error: The term "@f_equal2 nat nat Prop lt x1 y1 x2 y2 eq1 eq2" has type
>      "@eq Prop (lt x1 x2) (lt y1 y2)" while it is expected to have type
>      "@eq Type (lt x1 x2) (lt y1 y2)"


Best regards,
 Roman Beslik.