From 2ad56b995b00f21089bc8d0a2cbd84ec13979fa6 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 17 Feb 2020 20:32:11 +0100
Subject: [PATCH] `TopSet` instance for `boolset`.

---
 theories/boolset.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/boolset.v b/theories/boolset.v
index cd4efe1a..3bfa3b3d 100644
--- a/theories/boolset.v
+++ b/theories/boolset.v
@@ -19,15 +19,16 @@ Instance boolset_intersection {A} : Intersection (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && boolset_car X2 x).
 Instance boolset_difference {A} : Difference (boolset A) := λ X1 X2,
   BoolSet (λ x, boolset_car X1 x && negb (boolset_car X2 x)).
-Instance boolset_set `{EqDecision A} : Set_ A (boolset A).
+Instance boolset_top_set `{EqDecision A} : TopSet A (boolset A).
 Proof.
-  split; [split| |].
+  split; [split; [split| |]|].
   - by intros x ?.
   - by intros x y; rewrite <-(bool_decide_spec (x = y)).
   - split. apply orb_prop_elim. apply orb_prop_intro.
   - split. apply andb_prop_elim. apply andb_prop_intro.
   - intros X Y x; unfold elem_of, boolset_elem_of; simpl. 
     destruct (boolset_car X x), (boolset_car Y x); simpl; tauto.
+  - done.
 Qed.
 Instance boolset_elem_of_dec {A} : RelDecision (∈@{boolset A}).
 Proof. refine (λ x X, cast_if (decide (boolset_car X x))); done. Defined.
-- 
GitLab