The Coq mailing list

[Edsko de Vries <Edsko.de.Vries AT cs.tcd.ie>]

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

Remember that ~ is a function (~p is syntactic sugar for p -> False).  
Hence, you can do this reasoning step as follows:

Variable E p : Prop.

Lemma foo : (E -> p) -> (E /\ ~p -> False).
Proof.
  intros H1 H2.
  destruct H2 as (e, not_p).
  apply not_p.
  apply H1.
  apply e.
Qed.

Edsko