The Coq mailing list

[Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>]

Thanks for the explanation (to Adam as well). 

I hit this problem in an attempt to use Prop as impredicative Set. 
Having learned that the use of Set-valued nat confused me, 
I wonder if I can avoid them. 
Namely, is there a Prop-valued equivalent to nat and Z?

Best,
Keiko