The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

All,

The library Coq.Logic.Classical_Pred_Type gives a proof, using 
(propositional) excluded middle, that the negation of a forall is an exists:

Lemma not_all_ex_not :
 forall U:Type, forall P:U -> Prop, ~ (forall n:U, P n) -> exists n : U, ~ P 
n.

Does anyone know if the version of this that makes P predicative, using Type, 
is provable as well? That is, I am trying to prove:

Lemma not_all_ex_not_pred :
 forall U:Type, forall P:U -> Type, ((forall n:U, P n) -> False) -> exists n 
: U, P n -> False.

Thanks,
-Eddy