diff --git a/theories/base.v b/theories/base.v
index 7e9e59536fec4221aede1898ec0409cb12b85bce..86b1036fb2c416eb10b7c9f30377b42f52db988c 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -393,6 +393,8 @@ Proof. now intros -> ?. Qed.
 Instance unit_equiv : Equiv unit := λ _ _, True.
 Instance unit_equivalence : Equivalence (@equiv unit _).
 Proof. repeat split. Qed.
+Instance unit_leibniz : LeibnizEquiv unit.
+Proof. intros [] []; reflexivity. Qed.
 Instance unit_inhabited: Inhabited unit := populate ().
 
 (** ** Products *)