The Coq mailing list

[Matej Kosik <kosik AT fiit.stuba.sk>]

Hi,

In Coq, it is possible to make the following reasoning steps:

           E |- ~p
        E, p |- False

with the `intro' tactics. Both that lines above are meant to be
"sequents" where |- separates the antecedent and the succedent.

With what tactics can I perform the following reasoning step:

            E |- p
        E, ~p |- False

?

(I am new to Coq.)