The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Gyesik Lee wrote:
> > Why don't you just use [bool] instead of [Prop]?
> >
> >      
> because I want to have the property that there is no term of type
> [VarIn r] when its value is False.
> But this does not work with the Boolean [false].
>    

This property doesn't even type-check for [bool], but it's a mistake to 
conclude that it isn't easy to "use [bool]s as types."  Just use the 
boolean as the index to this type family:

    Inductive sing : bool -> Type := Sing : sing true.

There are other encodings you could consider, too.