The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 10/12/2014 20:04, Vadim Zaliva wrote:

> Lemma test (A:Type) `{Setoid A, Mult A} (x:A):
>    equiv (testF A A (mult x)) (testF A A (fun (x0:A) => mult x x0)) .
> Proof.
>    setoid_replace (fun (x0:A) => mult x x0) with (mult x).
> Qed.
>
> How one would define Proper instance to make this possible?
> It looks like I need something like FunctionalExtensionality.
>
> Thanks!
>
> P.S. Obviously this is artificial example just to demonstrate the kind
> of rewriting I am trying to do.

You presumably simplified your example too much, because this is a case 
of eta-conversion. So the "change" tactic will happily do the 
replacement. You do not need any setoid rewriting there.

Best regards,

Guillaume