The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 07/09/2014 03:37 PM, Guillaume Melquiond wrote:
> This kind of transformation is pointless. Because of the axiom
> Extensionality_Ensembles, you have A = B as soon as you have Same_set A B.
Since this axiom is still inconsistent with Coq, it may be a good idea 
to avoid it ;).

Anyway, making it work with setoids is easy: just declare Same_set as an 
equivalence relation, and prove that all operations on it respect it.

Require Import Ensembles Setoid Morphisms.

Instance: forall U, Equivalence (Same_set U).
Proof. firstorder. Qed.
Instance: forall U, Proper (Same_set U ==> eq ==> iff) (In U).
Proof. intros U A B ? x y ->; firstorder. Qed.

Goal forall U A B x, Same_set U A B -> In U A x -> In U B x.
Proof. intros U A B x H. rewrite H. easy. Qed.