From 12f82ad735531f59e82898366df84becf6fff1b6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 26 Aug 2019 13:42:37 +0200
Subject: [PATCH] add Equiv instance for Empty_set

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

diff --git a/theories/base.v b/theories/base.v
index 9a066b98..83847b69 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -591,6 +591,13 @@ Instance unit_leibniz : LeibnizEquiv unit.
 Proof. intros [] []; reflexivity. Qed.
 Instance unit_inhabited: Inhabited unit := populate ().
 
+(** ** Empty *)
+Instance Empty_set_equiv : Equiv Empty_set := λ _ _, True.
+Instance Empty_set_equivalence : Equivalence (≡@{Empty_set}).
+Proof. repeat split. Qed.
+Instance Empty_set_leibniz : LeibnizEquiv Empty_set.
+Proof. intros [] []; reflexivity. Qed.
+
 (** ** Products *)
 Notation "( x ,)" := (pair x) (only parsing) : stdpp_scope.
 Notation "(, y )" := (λ x, (x,y)) (only parsing) : stdpp_scope.
-- 
GitLab