The Coq mailing list

[Jiten Pathy <jpathy AT fssrv.net>]

Nice, Thank you.

On Tue, Jan 13, 2015 at 7:55 PM, Jonathan Leivent 
<jonikelee AT gmail.com>
 wrote:
>
> 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
>