coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] How to Prove "~~A <-> A"

From: hao chen <chrihop AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] How to Prove "~~A <-> A"
Date: Sat, 26 Oct 2013 17:54:49 +0800

Hi,

I am learning coq, but encounter a problem. I cannot prove "forall A, ~~A <-> A". 'exfalso', 'destruct' and 'intros' are all used, and I have searched it in google, but still cannot find the solution. Could someone tell me that is it provable? and how to prove it?

Thanks,

[Coq-Club] How to Prove "~~A <-> A", hao chen, 10/26/2013
- Re: [Coq-Club] How to Prove "~~A <-> A", Gabriel Scherer, 10/26/2013