The Coq mailing list

[muad <muad.dib.space AT gmail.com>]

> Hello to everyone.
> 
> 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).
> 
> Thanks in advance.

What is your actual goal and why do you want to do the rewrite.
-- 
View this message in context: 
http://www.nabble.com/Problem-with-rewriting-tp23853684p23861045.html
Sent from the Coq mailing list archive at Nabble.com.