The Coq mailing list

[Andr� Hirschowitz <ah AT unice.fr>]

>  
>
> I interprete this mistake as the violation of the typing rules, because
> Nat is probably of higher Type level as the X of its definition.
>
> Is this true ? Does a means exist for circumventing this problem ?

Hello,

Since "they" do not comment, let me say that I like the question, that I 
agree with your understanding of the error, and that I do not see any 
way around. So, this could eventually increase my interest in  the 
impredicative Set option.

ah