diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 60a087b43df6629ed76ebbe53adc9514ee1dae57..d8c8f241f8c635549c47049003612d487f1f1a9f 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1182,7 +1182,7 @@ Section map.
   Proof. apply big_opM_insert_delete. Qed.
 
   Lemma big_sepM_insert_2 Φ m i x :
-    TCOr (∀ x, Affine (Φ i x)) (Absorbing (Φ i x)) →
+    TCOr (∀ y, Affine (Φ i y)) (Absorbing (Φ i x)) →
     Φ i x -∗ ([∗ map] k↦y ∈ m, Φ k y) -∗ [∗ map] k↦y ∈ <[i:=x]> m, Φ k y.
   Proof.
     intros Ha. apply wand_intro_r. destruct (m !! i) as [y|] eqn:Hi; last first.
@@ -2091,6 +2091,30 @@ Section gset.
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ set] y ∈ X ∖ {[ x ]}, Φ y.
   Proof. apply big_opS_delete. Qed.
 
+  Lemma big_sepS_insert_2 {Φ X} x :
+    TCOr (Affine (Φ x)) (Absorbing (Φ x)) →
+    Φ x -∗ ([∗ set] y ∈ X, Φ y) -∗ ([∗ set] y ∈ {[ x ]} ∪ X, Φ y).
+  Proof.
+    intros Haff. apply wand_intro_r. destruct (decide (x ∈ X)); last first.
+    { rewrite -big_sepS_insert //. }
+    rewrite big_sepS_delete // assoc.
+    rewrite (sep_elim_l (Φ x)) -big_sepS_insert; last set_solver.
+    rewrite -union_difference_singleton_L //.
+    replace ({[x]} ∪ X) with X by set_solver.
+    auto.
+  Qed.
+
+  Lemma big_sepS_delete_2 {Φ X} x :
+    Affine (Φ x) →
+    Φ x -∗ ([∗ set] y ∈ X ∖ {[ x ]}, Φ y) -∗ [∗ set] y ∈ X, Φ y.
+  Proof.
+    intros Haff. apply wand_intro_r. destruct (decide (x ∈ X)).
+    { rewrite -big_sepS_delete //. }
+    rewrite sep_elim_r.
+    replace (X ∖ {[x]}) with X by set_solver.
+    auto.
+  Qed.
+
   Lemma big_sepS_elem_of Φ X x `{!Absorbing (Φ x)} :
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x.
   Proof. intros. rewrite big_sepS_delete //. by rewrite sep_elim_l. Qed.