在Coq最基本逻辑下这一条是无法证明的，原因在于Coq没有引入excluded_middle : forall P, P \/ ~P， 引入excluded_middle后的证明是平凡的。~~P ->P在库Logic.Classical内，为NNPP。