The Coq mailing list

[dimitrisg7 <dvekris AT hotmail.com>]

Pierre Castéran wrote:
> 
> I don't know whether it answers your initial questions, but if you 
> consider two logically equivalent
> propositions, you can replace one by another in a correct context (see 
> documentation on setoids):
> 
> 
> Require Import Setoid.
> Variables (x: Type)(K: nat -> Type).
> 
> Lemma L : (exists m, K m =x) <-> (exists n, x = K n).
> split;intros [m H];exists m;auto.
> Qed.
> 
> Variable P:Prop.
> Goal (exists m, K m =x) -> P.
> rewrite L.
> 
> 
> Admitted.
> 

I appreciate your help guys. What I was asking is a simple way to manipulate
this rewriting. Your answers have been really informative. 

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