From a0ee21d2d2a55c3d04295fd0e885c7bcccebcd72 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 15 Jan 2021 11:55:29 +0100
Subject: [PATCH] make use of new std++ lemmas

---
 iris/algebra/big_op.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/big_op.v b/iris/algebra/big_op.v
index 177fb8faa..bcd17298f 100644
--- a/iris/algebra/big_op.v
+++ b/iris/algebra/big_op.v
@@ -496,8 +496,9 @@ Lemma big_opS_set_map `{Countable A, Countable B} (h : A → B) (X : gset A) (f
   ([^o set] x ∈ set_map h X, f x) ≡ ([^o set] x ∈ X, f (h x)).
 Proof.
   intros Hinj.
-  induction X as [|x X ? IH] using set_ind_L => //=; [ by rewrite !big_opS_empty | ].
-  replace (set_map h ({[x]} ∪ X)) with ({[h x]} ∪ (set_map h X) : gset B) by set_solver.
+  induction X as [|x X ? IH] using set_ind_L.
+  { by rewrite set_map_empty !big_opS_empty. }
+  rewrite set_map_union_L set_map_singleton_L.
   rewrite !big_opS_union; [|set_solver..].
   rewrite !big_opS_singleton IH //.
 Qed.
-- 
GitLab