diff --git a/iris/cofe.v b/iris/cofe.v
index eb43c721c6cc29edf9bd2fd504214e3830e25143..7c48363ad033d2cf35899ea3a1fc73b0de85c789 100644
--- a/iris/cofe.v
+++ b/iris/cofe.v
@@ -272,6 +272,8 @@ Section discrete_cofe.
 End discrete_cofe.
 Arguments discrete_cofeC _ {_ _}.
 
+Definition leibniz_cofeC (A : Type) : cofeT := @discrete_cofeC A equivL _.
+
 (** Later *)
 Inductive later (A : Type) : Type := Later { later_car : A }.
 Arguments Later {_} _.
diff --git a/prelude/base.v b/prelude/base.v
index 497e040cf16b37389ac249afc901eb04e2a214c4..30ec94664e72c3f15ca1ea9847aa540e88a7c2cd 100644
--- a/prelude/base.v
+++ b/prelude/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. *)