$ rlwrap coqtop
Welcome to Coq 8.1pl2 (Oct. 2007)

Coq < Section Predicate_calculus.

Coq < Variable D:Set.
D is assumed

Coq < Variable P Q:D -> Prop.
P is assumed
Q is assumed

Coq < Theorem Ex1: (forall y:D, P y -> (forall x:D, ~ (P x)) -> Q y).
1 subgoal

  D : Set
  P : D -> Prop
  Q : D -> Prop
  ============================
   forall y : D, P y -> (forall x : D, ~ P x) -> Q y

Ex1 < intros.
1 subgoal

  D : Set
  P : D -> Prop
  Q : D -> Prop
  y : D
  H : P y
  H0 : forall x : D, ~ P x
  ============================
   Q y

(* Try to prove (Q y) by the "contradiction" tactics. *) 

Ex1 < contradiction.
Toplevel input, characters 0-13
> contradiction.
> ^^^^^^^^^^^^^
User error: No such contradiction

(* This fails. Coq does not see the consequence ~ P y.
   Therefore we prove ~ (P y) from the assumptions
   by the "assert" tactics. ~ (P y) becomes the new
   goal while Q y becomes a subgoal. *)


Ex1 < assert (~ (P y)).
2 subgoals

  D : Set
  P : D -> Prop
  Q : D -> Prop
  y : D
  H : P y
  H0 : forall x : D, ~ P x
  ============================
   ~ P y

subgoal 2 is:
 Q y


Ex1 < apply H0.
1 subgoal

  D : Set
  P : D -> Prop
  Q : D -> Prop
  y : D
  H : P y
  H0 : forall x : D, ~ P x
  H1 : ~ P y
  ============================
   Q y

(* Now Coq sees the contradiction. *)

Ex1 < contradiction.
Proof completed.

Ex1 < Save.
intros.
assert (~ P y).
 apply H0.
 contradiction.
Ex1 is defined

Coq <