パースの定理

パースの法則からcoqで排中律を導く。

Theorem Peirce : forall A B : Prop, ((A -> B) -> A) -> A.
Admitted.
Theorem classic : forall p : Prop, ~~p -> p.
Proof.
 unfold not.
 intros.  apply (Peirce p False).
 intro.  exfalso. apply H.  apply H0.
Qed.

SoftwareFoundation読み返したら、そのものずばりの問題があった。

でも、

Definition peirce := ∀ P Q: Prop,
  ((P→Q)->P)->P.

Theorem cl2 : forall P : Prop, ~~P -> P.
unfold not.
intros. apply (peirce P False).
-----------------------------------------------------
Toplevel input, characters 7-15:
Error: Illegal application (Non-functional construction): 
The expression "peirce" of type "Prop"
cannot be applied to the term
 "P" : "Prop"

書いてあるDefinitionでのPeirceだと、applyが使えない？なんで？