The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Richard,

below is a proof, that this is actually wrong. It gives a counter example, 
which shows where the problem is.

Best regards,

Michael

Lemma ThisIsWrong: 
  (forall (T:Set) (P:T->Prop), forall (x:T), P x -> (forall y, P y))
   -> False.
Proof.
  intros H.
  specialize (H bool).
  specialize (H (fun b => b=true)).
  specialize (H true).
  simpl in H.
  specialize (H eq_refl).
  specialize (H false).
  inversion H.
Qed.

Lemma ThisIsRight: 
  forall (T:Set) (P:T->Prop), (forall (x:T), P x) -> (forall y, P y).
Proof.
  intros T P H.
  assumption.
Qed.