coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: "...." <nixiejun AT 163.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?
Date: Sat, 23 Aug 2014 14:55:19 +0800 (CST)

Dear everyone:

I'mc confused with the following subgoal:

Theorem T1(P:Prop->Prop): forall B:Prop,~P B->~(exists A:Prop,P A).

Is it possible to prove?

Thank you ! Xiejun Ni.

[Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?, ...., 08/23/2014
- Re: [Coq-Club] What tactic can be used to prove 'forall' to '~ exists'?, Catalin Hritcu, 08/23/2014