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
.