The Coq mailing list

[Edsko de Vries <edskodevries AT gmail.com>]

Hi,

(exists n, K n = x) is syntactic sugar for ex (fun n : nat => eq (K n)  
x) and so *rewriting* would require rewriting under a binder (which  
requires extensionality)? However, it is easy to prove one from the  
other:

Section test.

Variable x : Type.
Variable K : nat -> Type.

Hypothesis H : exists n, K n = x.

Lemma foo : exists n, x = K n.
Proof.
  elim H ; intros n Hn.
  exists n ; apply sym_eq ; exact Hn.
Qed.

Hope that helps,

Edsko