The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/13/2015 10:29 PM, Jiten Pathy wrote:
> Hello,
> Trying to prove the following theorem from Software Foundations. A
> hint to proceed?
>
> https://gist.github.com/anonymous/42f75d0375ca8788cad6

Don't assert False yet.  First, intro x.  Then use H1 on (P x), and that 
will allow you to concentrate on what you can do with ~P x as a hypothesis.

-- Jonathan