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.