The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 10/14/2012 11:51 AM, Vincent Siles wrote:
> Using the lemma of Classical_Pred_Set.v,  Lemma not_ex_all_not : 
> forall P:U -> Prop, ~ (exists n : U, P n) -> forall n:U, ~ P n.
> I wanted to prove  (a more complicated lemma but it boils down to)
>
> Lemma foo (A:Set) (P : A -> Prop) : ~(exists x, exists y, exists z, (P 
> x /\ P y  /\ P z)) -> forall x y z, ~(P x /\ P y  /\ P z).

Perhaps your question is more about specific low-level tactics than 
about the best way to prove your examples, but I'll just point out that 
the built-in [firstorder] tactic proves either of these facts 
automatically, without appealing to axioms.