The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

There is another way to define bracket in Coq. Something like that:

Inductive bracket ( A : Type ) : Prop := wit : A -> bracket A .

 

Precisely that, indeed. It is, of course, equivalent to the impredicative definition Jeremy used.