From 4b0905e471122f3027af668591c8e99e48fb00bf 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.

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

diff --git a/theories/base.v b/theories/base.v
index 7e9e5953..86b1036f 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 *)
-- 
GitLab