The Coq mailing list

[Marcus Ramos <mvmramos AT gmail.com>]

Hi,

This should be obvious, but still I can´t see why it doesn´t work. In the script:

Lemma foo1:

forall (i j: nat), i=j -> (forall p q: nat, p <= q \/ p > q).

Proof.

Admitted.

Lemma foo2:

forall (m n: nat),

m = n -> n = m.

Proof.

intros m n H.

apply foo1 in H.

Why does the "apply foo1 in H" above causes the folowing error message to be displayed?

"Error: Unable to find an instance for the variables p, q."

Shouldn´t it just place (forall p q: nat, p <= q \/ p > q) in the context as a new hypothesis? If I execute, for example, apply foo1 with (p:=0)(q:=1) in H, I get H : 0 <= 1 \/ 0 > 1, but this is not what I want.

Thanks,

Marcus.