diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 7d61a954b994161ab34ac4bfa770092b96595186..629d448a997ddf3b014f8d9d7b0cdfb30ca4bf29 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -934,8 +934,8 @@ Section map2.
     - apply and_elim_r.
     - rewrite <- (left_id True%I (∧)%I (Φ i x1 x2)).
       apply and_mono=>//. apply pure_mono=>_ k.
-      rewrite !lookup_insert_is_Some' !lookup_empty.
-      firstorder.
+      rewrite !lookup_insert_is_Some' !lookup_empty -!not_eq_None_Some.
+      naive_solver.
   Qed.
 
   Lemma big_sepM2_fmap {A' B'} (f : A → A') (g : B → B') (Φ : nat → A' → B' → PROP) m1 m2 :