The Coq mailing list

[roconnor AT theorem.ca]

On Sun, 24 Jul 2005, Vladimir Voevodsky wrote:

> Can one prove a proposition of the form ~ Ex P for any P:T -> Prop at
> all?  E.g. can one prove ~ Ex le S(n) 0 where n:nat ?

Yes, absolutely.

Goal ~ ex (fun n => le (S n) 0).
intros [n P].
inversion P.
Qed.

In general ~ ex P is equivalent to forall x:T, ~(P x) (proof left as an
exercise).

-- 
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''