diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index e31916ec5c56af247daf34b44a99e28b46639b28..f5f422eef55899d1a0d547ba690ed3344e5aad62 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -1014,6 +1014,13 @@ Section and_list.
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_and PROP) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
 
+  Global Instance big_andL_nil_absorbing Φ :
+    Absorbing ([∧ list] k↦x ∈ [], Φ k x).
+  Proof. simpl; apply _. Qed.
+  Global Instance big_andL_absorbing Φ l :
+    (∀ k x, Absorbing (Φ k x)) → Absorbing ([∧ list] k↦x ∈ l, Φ k x).
+  Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
+
   Global Instance big_andL_nil_persistent Φ :
     Persistent ([∧ list] k↦x ∈ [], Φ k x).
   Proof. simpl; apply _. Qed.