1 files changed, 11 insertions, 1 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 4f794af3f..6270fb43b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -178,4 +178,14 @@ Section Respecting.
     symmetry. auto.
   Qed.
 
-End Respecting.
-\ No newline at end of file
+End Respecting.
+
+(** The default equivalence on function spaces. *)
+
+Program Instance [ Equivalence A eqA ] => 
+  pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA).
+
+  Next Obligation.
+  Proof.
+    transitivity (y x0) ; auto.
+  Qed.