diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 38139005f17f4b0536fe485933e3a2d7537776bc..a46cfcd9b77df3d417ef9f5da3bd35ab24b10818 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -739,7 +739,7 @@ Section map2.
   Lemma big_sepM2_dom Φ m1 m2 :
     ([∗ map] k↦y1;y2 ∈ m1; m2, Φ k y1 y2) -∗ ⌜ dom (gset K) m1 = dom (gset K) m2 ⌝.
   Proof.
-    rewrite /big_sepM2 bi.and_elim_l. apply pure_mono=>Hm.
+    rewrite /big_sepM2 and_elim_l. apply pure_mono=>Hm.
     set_unfold=>k. by rewrite !elem_of_dom.
   Qed.
 
@@ -747,7 +747,7 @@ Section map2.
     (∀ k y1 y2, m1 !! k = Some y1 → m2 !! k = Some y2 → Φ k y1 y2 ⊢ Ψ k y1 y2) →
     ([∗ map] k ↦ y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢ [∗ map] k ↦ y1;y2 ∈ m1;m2, Ψ k y1 y2.
   Proof.
-    intros Hm1m2. rewrite /big_sepM2. apply bi.and_mono_r, big_sepM_mono.
+    intros Hm1m2. rewrite /big_sepM2. apply and_mono_r, big_sepM_mono.
     intros k [x1 x2]. rewrite map_lookup_zip_with.
     specialize (Hm1m2 k x1 x2).
     destruct (m1 !! k) as [y1|]; last done.
@@ -792,21 +792,15 @@ Section map2.
   Lemma big_sepM2_empty_l m1 Φ :
     ([∗ map] k↦y1;y2 ∈ m1; ∅, Φ k y1 y2) ⊢ ⌜m1 = ∅⌝.
   Proof.
-    rewrite /big_sepM2 and_elim_l.
-    apply pure_elim'=>Hm1. apply pure_mono=>_.
-    apply map_eq=>k. specialize (Hm1 k). revert Hm1.
-    rewrite !lookup_empty /=. destruct (m1 !! k) as [x|]; last done.
-    intros Hm1. exfalso. eapply is_Some_None, Hm1. eauto.
+    rewrite big_sepM2_dom dom_empty_L.
+    apply pure_mono, dom_empty_inv_L.
   Qed.
 
   Lemma big_sepM2_empty_r m2 Φ :
     ([∗ map] k↦y1;y2 ∈ ∅; m2, Φ k y1 y2) ⊢ ⌜m2 = ∅⌝.
   Proof.
-    rewrite /big_sepM2 and_elim_l.
-    apply pure_elim'=>Hm2. apply pure_mono=>_.
-    apply map_eq=>k. specialize (Hm2 k). revert Hm2.
-    rewrite !lookup_empty /=. destruct (m2 !! k) as [x|]; last done.
-    intros Hm2. exfalso. eapply is_Some_None, Hm2. eauto.
+    rewrite big_sepM2_dom dom_empty_L.
+    apply pure_mono=>?. eapply (dom_empty_inv_L (D:=gset K)). eauto.
   Qed.
 
   Lemma big_sepM2_insert Φ m1 m2 i x1 x2 :
@@ -888,7 +882,7 @@ Section map2.
     ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2) ⊢
     Φ i x1 x2 ∗ (Φ i x1 x2 -∗ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k y1 y2)).
   Proof.
-    intros Hm1 Hm2. etransitivity; first apply big_sepM2_insert_acc=>//.
+    intros Hm1 Hm2. etrans; first apply big_sepM2_insert_acc=>//.
     apply sep_mono_r. rewrite (forall_elim x1) (forall_elim x2).
     rewrite !insert_id //.
  Qed.
@@ -937,9 +931,9 @@ Section map2.
   Proof.
     rewrite /big_sepM2 map_zip_with_singleton big_sepM_singleton.
     apply (anti_symm _).
-    - apply bi.and_elim_r.
+    - apply and_elim_r.
     - rewrite <- (left_id True%I (∧)%I (Φ i x1 x2)).
-      apply bi.and_mono=>//. apply pure_mono=>_ k.
+      apply and_mono=>//. apply pure_mono=>_ k.
       rewrite !lookup_insert_is_Some' !lookup_empty.
       firstorder.
   Qed.
@@ -949,7 +943,7 @@ Section map2.
     ⊣⊢ ([∗ map] k↦y1;y2 ∈ m1;m2, Φ k (f y1) (g y2)).
   Proof.
     rewrite /big_sepM2. rewrite map_fmap_zip.
-    apply bi.and_proper.
+    apply and_proper.
     - apply pure_proper. split.
       + intros Hm k. specialize (Hm k). revert Hm.
         by rewrite !lookup_fmap !fmap_is_Some.
@@ -976,9 +970,9 @@ Section map2.
     rewrite -{1}(and_idem ⌜∀ k : K, is_Some (m1 !! k) ↔ is_Some (m2 !! k)⌝%I).
     rewrite -and_assoc.
     rewrite !persistent_and_affinely_sep_l /=.
-    rewrite -sep_assoc. apply bi.sep_proper=>//.
+    rewrite -sep_assoc. apply sep_proper=>//.
     rewrite sep_assoc (sep_comm _ (<affine> _)%I) -sep_assoc.
-    apply bi.sep_proper=>//. apply big_sepM_sepM.
+    apply sep_proper=>//. apply big_sepM_sepM.
   Qed.
 
   Lemma big_sepM2_and Φ Ψ m1 m2 :
@@ -1361,14 +1355,14 @@ Section list2.
   Lemma big_sepL2_later_2 Φ l1 l2 :
     ([∗ list] k↦y1;y2 ∈ l1;l2, ▷ Φ k y1 y2) ⊢ ▷ [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
   Proof.
-    rewrite !big_sepL2_alt bi.later_and big_sepL_later_2.
+    rewrite !big_sepL2_alt later_and big_sepL_later_2.
     auto using and_mono, later_intro.
   Qed.
 
   Lemma big_sepL2_laterN_2 Φ n l1 l2 :
     ([∗ list] k↦y1;y2 ∈ l1;l2, ▷^n Φ k y1 y2) ⊢ ▷^n [∗ list] k↦y1;y2 ∈ l1;l2, Φ k y1 y2.
   Proof.
-    rewrite !big_sepL2_alt bi.laterN_and big_sepL_laterN_2.
+    rewrite !big_sepL2_alt laterN_and big_sepL_laterN_2.
     auto using and_mono, laterN_intro.
   Qed.