The Coq mailing list

[Loic Pottier <loic.pottier AT sophia.inria.fr>]

Hi,
suppose we have:

Definition part(E:Type):= E ->Prop.

then can one write something like 

forall `(A:part E), True

in order to get E generalized automatically, like it works in arguments 
of  Type Classes?

Loïc