From bfad9bffcaed96789166854c9f7afe4e5cbe9ccc Mon Sep 17 00:00:00 2001
From: Amin Timany <amintimany@gmail.com>
Date: Wed, 14 Sep 2016 13:01:38 +0200
Subject: [PATCH] In gset idemp_L rather than union_idem_L
---
algebra/gset.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/algebra/gset.v b/algebra/gset.v
index a00ced785..1ee25c530 100644
--- a/algebra/gset.v
+++ b/algebra/gset.v
@@ -32,7 +32,7 @@ Section gset.
- solve_proper.
- intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
- intros X1 X2. by rewrite !gset_op_union comm_L.
- - intros X. by rewrite gset_op_union gset_core_self union_idemp_L.
+ - intros X. by rewrite gset_core_self idemp_L.
Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
--
GitLab