The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 04.10.2012 16:46, schrieb Matthieu Sozeau:
> On 4 oct. 2012, at 09:54, Jonas Oberhauser 
> <s9joober AT gmail.com>
>  wrote:
>
> > Hi all,
> >
> > is there such a thing like a replace at?
> >
> >   Goal forall X (x y : X) P, P x y -> x = y -> P x x.
> >   intros.
> >   replace x with y at 2. (* doesn't work ? *)
> >   rewrite H at 2. (* supposedly requries Setoid ? *)
> Hi,
>    indeed the at requires Setoid, and there is a variant
> [setoid_replace] defined in theories/Classes/SetoidTactics.v.
> It will rewrite with standard leibniz equality just as well
> as rewrite.
>
> Best,
> -- Matthieu

Thanks a lot! This is interesting. Why is that?
Kind regards, jonas