I’m having trouble understanding why I can’t prove a particular lemma:

```
Definition gen_prop := forall (X : Type) (p1 p2 : X -> X -> Prop),
(forall x y, p1 x y <-> p2 x y) ->
(forall x y, p2 x y -> False) ->
(forall x y, p1 x y) -> False.
Lemma gen_prop_contra : gen_prop.
Proof.
intros X p1 p2 H1 H2 H3.
eapply H1 in H3. apply H2 in H3. assumption.
Unshelve.
Abort.
2 goals
X : Type
p1, p2 : X -> X -> Prop
H1 : forall x y : X, p1 x y <-> p2 x y
H2 : forall x y : X, p2 x y -> False
______________________________________(1/2)
X
______________________________________(2/2)
X
```

So, I need an “example” instance of an X in order for this proof to work. E.g.:

```
Definition gen_prop' := forall (X : Type) (z : X )(p1 p2 : X -> X -> Prop),
(forall x y, p1 x y <-> p2 x y) ->
(forall x y, p2 x y -> False) ->
(forall x y, p1 x y) -> False.
Lemma gen_prop_contra' : gen_prop'.
Proof.
intros X z p1 p2 H1 H2 H3.
eapply H1 in H3. apply H2 in H3. assumption.
Unshelve.
all: assumption.
Qed.
```

I don’t understand why that is required. The non-quantified version is automatic:

```
Lemma prop_contra : forall p1 p2 : Prop,
(p1 <-> p2) -> (p2 -> False) -> p1 -> False.
Proof. intuition. Qed.
```

And the quantified version is automatic as long as I keep the quantification “outside”:

```
Definition gen_prop_outer_quant := forall (X : Type)
(p1 p2 : X -> X -> Prop)
(x y : X),
(p1 x y <-> p2 x y) ->
(p2 x y -> False) ->
p1 x y -> False.
Lemma gen_prop_outer_contra : gen_prop_outer_quant.
Proof. intros X p1 p2 x y. intuition. Qed.
```

Similarly, if I’m working with a concrete type, e.g. `nat`

, I can supply my own example as part of the proof:

```
Definition nat_prop' :=
forall p1 p2 : nat -> nat -> Prop,
(forall x y, p1 x y <-> p2 x y) ->
(forall x y, p2 x y -> False) ->
(forall x y, p1 x y) -> False.
Lemma nat_prop_contra : nat_prop'.
Proof.
intros p1 p2 H1 H2 H3.
specialize H1 with (x := 0).
specialize H1 with (y := 1).
apply H1 in H3. apply H2 in H3.
assumption.
Qed.
```

But I still don’t understand why I need to supply a `nat`

at all here.

Structurally, the quantified one I want to prove seems like the same proof as the propositional version. And the additional quantifier I have to add to make Coq accept the proof doesn’t seem to contribute anything meaningful.

Am I doing the proof wrong? Or am I failing to understand something about the underlying logical system that makes my initial version invalid?

Any insight would be appreciated.