From 72a0502367c53bee2ffa90f39140ca38f760262c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 11 Jul 2016 15:09:15 +0200
Subject: [PATCH] LeibnizEquiv instance for unit.

---
 prelude/base.v | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prelude/base.v b/prelude/base.v
index 7e9e59536..86b1036fb 100644
--- a/prelude/base.v
+++ b/prelude/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 *)
-- 
GitLab