# How to prove forall P : Prop, ~~P -> P

I am completely new to coq programming and was trying to solve below logic problem.

```
Theorem nnp_imp_p : forall P : Prop, ~~P -> P.
Proof.
unfold not.
intros P P_implies_F_implies_F.
Abort.
On coq console I saw the subgoal as
1 subgoal
P : Prop
P_implies_F_implies_F : (P -> False) -> False
______________________________________(1/1)
P
```

After this I am unable to prove anything...does that mean given logic cannot be provable using coq or I am doing something wrong? Because with classical logic using truth table we can easily prove it.... Please suggest....