The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

dimitrisg7 wrote:
> This is my context (x: Type)(K: nat -> Type).
> I would like to know how to rewrite (exists n, K n = x) as (exists m, x = K
> m).
>   

Without proof irrelevance or some other axiom, you can't prove that 
these two propositions are equal, which makes it impossible to do 
"rewriting" in the usual sense.