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....