Library Coq.Classes.SetoidAxioms
Require Import Coq.Program.Program.
Require Export Coq.Classes.SetoidClass.
Axiom setoideq_eq : forall `{sa : Setoid a} (x y : a), x == y -> x = y.
Application of the extensionality principle for setoids.
Ltac setoid_extensionality :=
match goal with
[ |- @eq ?A ?X ?Y ] => apply (setoideq_eq (a:=A) (x:=X) (y:=Y))
end.