coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with rewriting

From: dimitrisg7 <dvekris AT hotmail.com>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Problem with rewriting
Date: Wed, 3 Jun 2009 08:28:38 -0700 (PDT)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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.

-----
Never say never.
--
View this message in context:
http://www.nabble.com/Problem-with-rewriting-tp23853684p23853684.html
Sent from the Coq mailing list archive at Nabble.com.

[Coq-Club] Problem with rewriting, dimitrisg7
- Re: [Coq-Club] Problem with rewriting, Edsko de Vries
- Re: [Coq-Club] Problem with rewriting, Adam Chlipala
- Re: [Coq-Club] Problem with rewriting, muad
  - Re: [Coq-Club] Problem with rewriting, Pierre Casteran
    - Re: [Coq-Club] Problem with rewriting, dimitrisg7
- Re: [Coq-Club] Problem with rewriting, dimitrisg7
  - Re: [Coq-Club] Problem with rewriting, Adam Chlipala