diff --git a/theories/base.v b/theories/base.v
index 497e040cf16b37389ac249afc901eb04e2a214c4..30ec94664e72c3f15ca1ea9847aa540e88a7c2cd 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -194,6 +194,8 @@ Ltac unfold_leibniz := repeat
     setoid_rewrite <-(leibniz_equiv (A:=A))
   end.
 
+Definition equivL {A} : Equiv A := (=).
+
 (** A [Params f n] instance forces the setoid rewriting mechanism not to
 rewrite in the first [n] arguments of the function [f]. We will declare such
 instances for all operational type classes in this development. *)