这个引理可以证明建设性地。如果您考虑可以采取哪些步骤来取得进步，引理就证明了自己：

This lemma can be proved constructively. If you think about what can be done at each step to make progress the lemma proves itself:

Lemma PeirceContra :
  forall P Q, ~P -> ~((P -> Q) -> P).
Proof.
  intros P Q np.
  unfold "~".
  intros pq_p.
  apply np.     (* this is pretty much the only thing we can do at this point *)
  apply pq_p.   (* this is almost inevitable too *)

  (* the rest should be easy *)
(* Qed. *)