Ohad : "More formally, intuitionistic logic explicitly negates the law of excluded middle."
HMC : "Erm, no.  It does not have "not (p or (not p))" as an axiom, as this statement would suggest."
Ohad : "is not an axiom but follows from the axioms in few steps. is in the literature all over...."

Theorem Ohad_Is_Wrong : forall P : Prop, not (not (P + not P)).
Proof.
 intros P.
 unfold not.
 intros f.
 refine (f _ ).
 right.
 intros p.
 refine (f (inl P (P->False) p)).
Qed.