The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Is there a standard name in Coq for the following:

Inductive nonempty (T:Type) : Prop := wtns: T -> nonempty T. 

?

Thanks!
Vladimir.