Commit bfad9bff authored by Amin Timany's avatar Amin Timany

In gset idemp_L rather than union_idem_L

parent 2c64b551
...@@ -32,7 +32,7 @@ Section gset. ...@@ -32,7 +32,7 @@ Section gset.
- solve_proper. - solve_proper.
- intros X1 X2 X3. by rewrite !gset_op_union assoc_L. - intros X1 X2 X3. by rewrite !gset_op_union assoc_L.
- intros X1 X2. by rewrite !gset_op_union comm_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. Qed.
Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin. Canonical Structure gsetR := discreteR (gset K) gset_ra_mixin.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment