When I run the Coq script below (a simplification of the original one):
Inductive w (g: nat): nat -> Prop:=
| z: w g 0.
Lemma x:
forall (i j: nat), w i j -> (forall k: nat, k <= k).
Proof.
Admitted.
Lemma y:
forall (m n: nat),
w m n -> w m n.
Proof.
intros m n H.
apply x in H.
I get the following error message on the last line:
Error: Unable to find an instance for the variable k.
Can anybody explain to me why this happens and what I have to do in order to have forall k: nat, k <= k
as a new hypothesis in the context?
Thanks in advance, Marcus.