diff options
Diffstat (limited to 'theories/Classes')
-rw-r--r-- | theories/Classes/Equivalence.v | 12 |
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. |