The Coq mailing list

[Param Jyothi Reddy <paramr AT gmail.com>]

Hi all, I was trying to understand how in intutionistic logic 
     (forall P)(P(x)->P(y)) |- (forall P)(P(y)->P(x))
is true. In classical logic this follows from (not P->not Q |- P->Q)

So i took a look at how Coq proves this.
(http://www.labri.fr/Perso/~casteran/CoqArt/depprod/SRC/leibniz.v)

i got

leibniz_sym < intros a b H Q.
1 subgoal

  A : Set
  a : A
  b : A
  H : forall P : A -> Prop, P a -> P b
  Q : A -> Prop
  ============================
   Q b -> Q a

leibniz_sym < apply H.
1 subgoal

  A : Set
  a : A
  b : A
  H : forall P : A -> Prop, P a -> P b
  Q : A -> Prop
  ============================
   Q a -> Q a

I am unable to understand how apply H resulted in Q a-> Q a. (My
expectation was H applied to Q would be Q a -> Q b)

Can someone throw more light on this and how to prove symmetry?

Param