The Coq mailing list

[Vincent BENAYOUN <benayoun.vincent AT gmail.com>]

Hi all,

I don't understand clearly why I cannot prove the following Lemma, which seems to be a kind of "axiom of dependent choice".

I will be glad if somebody can enlighten me, why I cannot instantiate the existential variable with x0.

I get the following type error :

Toplevel input, characters 16-18:

Error: Instance is not well-typed in the environment of ?9649

Lemma exists_fun :

  forall (P:nat->nat->Prop),

    (forall (x:nat), exists (v:nat), P x v)

    -> exists (f:nat->nat), forall (x:nat), P x (f x).

Proof.

  intros P H.

  refine(ex_intro (fun (f:nat->nat) => forall x : nat, P x (f x)) (fun x => _) _).

  intros x.

  specialize (H x).

  inversion H.

  instantiate (1:=x0).

Thanks in advance,

Vincent