diff --git a/CHANGELOG.md b/CHANGELOG.md
index 162142ed4d3228626fce4a28941389e4740f854a..55208174eb36c1f0cf309b13c4042bc2e75c9b14 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,14 @@ lemma.
 
 ## Iris master
 
+**Changes in `bi`:**
+
+* Generalize `big_op` lemmas that were previously assuming `Absorbing`ness of
+  some assertion: they now take any of (`TCOr`) an `Affine` instance or an
+  `Absorbing` instance. This breaks uses where an `Absorbing` instance was
+  provided without relying on TC search (e.g. in `by apply ...`; a possible fix
+  is `by apply: ...`). (by Glen Mével, Bedrock Systems)
+
 **Changes in `proofmode`:**
 
 * `iAssumption` no longer instantiates evar premises with `False`. This used
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 578d4a71575ccd2accccd82ffc3b41d2c1cc4d3b..3fd8c60160ff40901f0a38c04457fec99282125e 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -186,14 +186,23 @@ Section sep_list.
     ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x ∗ (Φ i x -∗ ([∗ list] k↦y ∈ l, Φ k y)).
   Proof. intros. by rewrite {1}big_sepL_insert_acc // (forall_elim x) list_insert_id. Qed.
 
-  Lemma big_sepL_lookup Φ l i x `{!Absorbing (Φ i x)} :
+  Lemma big_sepL_lookup Φ l i x
+    `{!TCOr (∀ j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
     l !! i = Some x → ([∗ list] k↦y ∈ l, Φ k y) ⊢ Φ i x.
-  Proof. intros. rewrite big_sepL_lookup_acc //. by rewrite sep_elim_l. Qed.
+  Proof.
+    intros Hi. destruct select (TCOr _ _).
+    - rewrite -(take_drop_middle l i x) // big_sepL_app /= take_length.
+      apply lookup_lt_Some in Hi. rewrite (_ : _ + 0 = i); last lia.
+      rewrite sep_elim_r sep_elim_l //.
+    - rewrite big_sepL_lookup_acc // sep_elim_l //.
+  Qed.
 
-  Lemma big_sepL_elem_of (Φ : A → PROP) l x `{!Absorbing (Φ x)} :
+  Lemma big_sepL_elem_of (Φ : A → PROP) l x
+    `{!TCOr (∀ y, Affine (Φ y)) (Absorbing (Φ x))} :
     x ∈ l → ([∗ list] y ∈ l, Φ y) ⊢ Φ x.
   Proof.
-    intros [i ?]%elem_of_list_lookup. by eapply (big_sepL_lookup (λ _, Φ)).
+    intros [i ?]%elem_of_list_lookup.
+    destruct select (TCOr _ _); by apply: big_sepL_lookup.
   Qed.
 
   Lemma big_sepL_fmap {B} (f : A → B) (Φ : nat → B → PROP) l :
@@ -627,10 +636,19 @@ Section sep_list2.
     by rewrite !list_insert_id.
   Qed.
 
-  Lemma big_sepL2_lookup Φ l1 l2 i x1 x2 `{!Absorbing (Φ i x1 x2)} :
+  Lemma big_sepL2_lookup Φ l1 l2 i x1 x2
+    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (Absorbing (Φ i x1 x2))} :
     l1 !! i = Some x1 → l2 !! i = Some x2 →
     ([∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2) ⊢ Φ i x1 x2.
-  Proof. intros. rewrite big_sepL2_lookup_acc //. by rewrite sep_elim_l. Qed.
+  Proof.
+    intros Hx1 Hx2. destruct select (TCOr _ _).
+    - rewrite -(take_drop_middle l1 i x1) // -(take_drop_middle l2 i x2) //.
+      apply lookup_lt_Some in Hx1. apply lookup_lt_Some in Hx2.
+      rewrite big_sepL2_app_same_length /= 2?take_length; last lia.
+      rewrite (_ : _ + 0 = i); last lia.
+      rewrite sep_elim_r sep_elim_l //.
+    - rewrite big_sepL2_lookup_acc // sep_elim_l //.
+  Qed.
 
   Lemma big_sepL2_fmap_l {A'} (f : A → A') (Φ : nat → A' → B → PROP) l1 l2 :
     ([∗ list] k↦y1;y2 ∈ f <$> l1; l2, Φ k y1 y2)
@@ -1317,14 +1335,14 @@ Section sep_map.
     ([∗ map] k↦y ∈ <[i:=x]> m, Φ k y) ⊣⊢ Φ i x ∗ [∗ map] k↦y ∈ delete i m, Φ k y.
   Proof. apply big_opM_insert_delete. Qed.
 
-  Lemma big_sepM_insert_2 Φ m i x :
-    TCOr (∀ y, Affine (Φ i y)) (Absorbing (Φ i x)) →
+  Lemma big_sepM_insert_2 Φ m 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.
+    apply wand_intro_r. destruct (m !! i) as [y|] eqn:Hi; last first.
     { by rewrite -big_sepM_insert. }
     assert (TCOr (Affine (Φ i y)) (Absorbing (Φ i x))).
-    { destruct Ha; try apply _. }
+    { destruct select (TCOr _ _); apply _. }
     rewrite big_sepM_delete // assoc.
     rewrite (sep_elim_l (Φ i x)) -big_sepM_insert ?lookup_delete //.
     by rewrite insert_delete_insert.
@@ -1337,13 +1355,19 @@ Section sep_map.
     intros. rewrite big_sepM_delete //. by apply sep_mono_r, wand_intro_l.
   Qed.
 
-  Lemma big_sepM_lookup Φ m i x `{!Absorbing (Φ i x)} :
+  Lemma big_sepM_lookup Φ m i x
+    `{!TCOr (∀ j y, Affine (Φ j y)) (Absorbing (Φ i x))} :
     m !! i = Some x → ([∗ map] k↦y ∈ m, Φ k y) ⊢ Φ i x.
-  Proof. intros. rewrite big_sepM_lookup_acc //. by rewrite sep_elim_l. Qed.
+  Proof.
+    intros Hi. destruct select (TCOr _ _).
+    - rewrite big_sepM_delete // sep_elim_l //.
+    - rewrite big_sepM_lookup_acc // sep_elim_l //.
+  Qed.
 
-  Lemma big_sepM_lookup_dom (Φ : K → PROP) m i `{!Absorbing (Φ i)} :
+  Lemma big_sepM_lookup_dom (Φ : K → PROP) m i
+    `{!TCOr (∀ j, Affine (Φ j)) (Absorbing (Φ i))} :
     is_Some (m !! i) → ([∗ map] k↦_ ∈ m, Φ k) ⊢ Φ i.
-  Proof. intros [x ?]. by eapply (big_sepM_lookup (λ i x, Φ i)). Qed.
+  Proof. intros [x ?]. destruct select (TCOr _ _); by apply: big_sepM_lookup. Qed.
 
   Lemma big_sepM_singleton Φ i x : ([∗ map] k↦y ∈ {[i:=x]}, Φ k y) ⊣⊢ Φ i x.
   Proof. by rewrite big_opM_singleton. Qed.
@@ -2075,15 +2099,15 @@ Section map2.
     by apply wand_intro_l.
   Qed.
 
-  Lemma big_sepM2_insert_2 Φ m1 m2 i x1 x2 :
-    TCOr (∀ x y, Affine (Φ i x y)) (Absorbing (Φ i x1 x2)) →
+  Lemma big_sepM2_insert_2 Φ m1 m2 i x1 x2
+    `{!TCOr (∀ x y, Affine (Φ i x y)) (Absorbing (Φ i x1 x2))} :
     Φ i x1 x2 -∗
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) -∗
     ([∗ map] k↦y1;y2 ∈ <[i:=x1]>m1; <[i:=x2]>m2, Φ k y1 y2).
   Proof.
-    intros Ha. rewrite big_sepM2_eq /big_sepM2_def.
+    rewrite big_sepM2_eq /big_sepM2_def.
     assert (TCOr (∀ x, Affine (Φ i x.1 x.2)) (Absorbing (Φ i x1 x2))).
-    { destruct Ha; try apply _. }
+    { destruct select (TCOr _ _); apply _. }
     apply wand_intro_r.
     rewrite !persistent_and_affinely_sep_l /=.
     rewrite (sep_comm  (Φ _ _ _)) -sep_assoc. apply sep_mono.
@@ -2103,25 +2127,32 @@ Section map2.
     rewrite !insert_id //.
  Qed.
 
-  Lemma big_sepM2_lookup Φ m1 m2 i x1 x2 `{!Absorbing (Φ i x1 x2)} :
+  Lemma big_sepM2_lookup Φ m1 m2 i x1 x2
+    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (Absorbing (Φ i x1 x2))} :
     m1 !! i = Some x1 → m2 !! i = Some x2 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ Φ i x1 x2.
-  Proof. intros. rewrite big_sepM2_lookup_acc //. by rewrite sep_elim_l. Qed.
-  Lemma big_sepM2_lookup_l Φ m1 m2 i x1 `{!∀ x2, Absorbing (Φ i x1 x2)} :
+  Proof.
+    intros Hx1 Hx2. destruct select (TCOr _ _).
+    - rewrite big_sepM2_delete // sep_elim_l //.
+    - rewrite big_sepM2_lookup_acc // sep_elim_l //.
+  Qed.
+  Lemma big_sepM2_lookup_l Φ m1 m2 i x1
+    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (∀ x2, Absorbing (Φ i x1 x2))} :
     m1 !! i = Some x1 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊢ ∃ x2, ⌜m2 !! i = Some x2⌝ ∧ Φ i x1 x2.
   Proof.
     intros Hm1. rewrite big_sepM2_delete_l //.
-    f_equiv=> x2. by rewrite sep_elim_l.
+    f_equiv=> x2. destruct select (TCOr _ _); by rewrite sep_elim_l.
   Qed.
-  Lemma big_sepM2_lookup_r Φ m1 m2 i x2 `{!∀ x1, Absorbing (Φ i x1 x2)} :
+  Lemma big_sepM2_lookup_r Φ m1 m2 i x2
+    `{!TCOr (∀ j y1 y2, Affine (Φ j y1 y2)) (∀ x1, Absorbing (Φ i x1 x2))} :
     m2 !! i = Some x2 →
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)
     ⊢ ∃ x1, ⌜m1 !! i = Some x1⌝ ∧ Φ i x1 x2.
   Proof.
     intros Hm2. rewrite big_sepM2_delete_r //.
-    f_equiv=> x1. by rewrite sep_elim_l.
+    f_equiv=> x1. destruct select (TCOr _ _); by rewrite sep_elim_l.
   Qed.
 
   Lemma big_sepM2_singleton Φ i x1 x2 :
@@ -2505,11 +2536,11 @@ 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)) →
+  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.
+    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.
@@ -2529,9 +2560,13 @@ Section gset.
     auto.
   Qed.
 
-  Lemma big_sepS_elem_of Φ X x `{!Absorbing (Φ x)} :
+  Lemma big_sepS_elem_of Φ X x
+    `{!TCOr (∀ y, Affine (Φ y)) (Absorbing (Φ x))} :
     x ∈ X → ([∗ set] y ∈ X, Φ y) ⊢ Φ x.
-  Proof. intros. rewrite big_sepS_delete //. by rewrite sep_elim_l. Qed.
+  Proof.
+    intros ?. rewrite big_sepS_delete //.
+    destruct select (TCOr _ _); by rewrite sep_elim_l.
+  Qed.
 
   Lemma big_sepS_elem_of_acc Φ X x :
     x ∈ X →
@@ -2788,9 +2823,13 @@ Section gmultiset.
     x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊣⊢ Φ x ∗ [∗ mset] y ∈ X ∖ {[+ x +]}, Φ y.
   Proof. apply big_opMS_delete. Qed.
 
-  Lemma big_sepMS_elem_of Φ X x `{!Absorbing (Φ x)} :
+  Lemma big_sepMS_elem_of Φ X x
+    `{!TCOr (∀ y, Affine (Φ y)) (Absorbing (Φ x))} :
     x ∈ X → ([∗ mset] y ∈ X, Φ y) ⊢ Φ x.
-  Proof. intros. rewrite big_sepMS_delete //. by rewrite sep_elim_l. Qed.
+  Proof.
+    intros ?. rewrite big_sepMS_delete //.
+    destruct select (TCOr _ _); by rewrite sep_elim_l.
+  Qed.
 
   Lemma big_sepMS_elem_of_acc Φ X x :
     x ∈ X →