diff --git a/CHANGELOG.md b/CHANGELOG.md
index 914e342653d36c58cac59a6ea5279a05805b921b..4376cb470620679cc73f3a3cdaf605acf2f01658 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -16,6 +16,9 @@ lemma.
 
 * Add lemma `na_own_empty` and persistence instance for `na_own p ∅` for
   non-atomic invariant tokens. (by Benjamin Peters)
+* Add instances `big_sepL_flip_mono'`, `big_sepM_flip_mono'`, etc., which are
+  wrappers of instances `big_sep*_mono'` for `flip (⊢)` instead of `(⊢)`. (by
+  Yusuke Matsushita)
 
 **Infrastructure:**
 
diff --git a/iris/bi/big_op.v b/iris/bi/big_op.v
index 7de10fb20d378d9c1d5dd1f048b7036e98f55c67..ed494942484509192fac2489c82c73165675c4f4 100644
--- a/iris/bi/big_op.v
+++ b/iris/bi/big_op.v
@@ -130,6 +130,10 @@ Section sep_list.
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
            (big_opL (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_sepL_mono; intros; apply Hf. Qed.
+  Global Instance big_sepL_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (flip (⊢))) ==> (=) ==> flip (⊢))
+           (big_opL (@bi_sep PROP) (A:=A)).
+  Proof. solve_proper. Qed.
   Global Instance big_sepL_id_mono' :
     Proper (Forall2 (⊢) ==> (⊢)) (big_opL (@bi_sep PROP) (λ _ P, P)).
   Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
@@ -606,6 +610,11 @@ Section sep_list2.
       ==> (=) ==> (=) ==> (⊢))
            (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
   Proof. intros f g Hf l1 ? <- l2 ? <-. apply big_sepL2_mono; intros; apply Hf. Qed.
+  Global Instance big_sepL2_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (flip (⊢))))
+            ==> (=) ==> (=) ==> flip (⊢))
+           (big_sepL2 (PROP:=PROP) (A:=A) (B:=B)).
+  Proof. solve_proper. Qed.
   Global Instance big_sepL2_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
       ==> (=) ==> (=) ==> (⊣⊢))
@@ -1352,6 +1361,10 @@ Section sep_map.
     Proper (pointwise_relation _ (pointwise_relation _ (⊢)) ==> (=) ==> (⊢))
            (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
   Proof. intros f g Hf m ? <-. apply big_sepM_mono; intros; apply Hf. Qed.
+  Global Instance big_sepM_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (flip (⊢))) ==> (=) ==> flip (⊢))
+           (big_opM (@bi_sep PROP) (K:=K) (A:=A)).
+  Proof. solve_proper. Qed.
 
   Global Instance big_sepM_empty_persistent Φ :
     Persistent ([∗ map] k↦x ∈ ∅, Φ k x).
@@ -2082,9 +2095,15 @@ Section map2.
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊢)))
       ==> (=) ==> (=) ==> (⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_mono; intros; apply Hf. Qed.
+  Global Instance big_sepM2_flip_mono' :
+    Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (flip (⊢))))
+            ==> (=) ==> (=) ==> flip (⊢))
+           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
+  Proof. solve_proper. Qed.
   Global Instance big_sepM2_proper' :
     Proper (pointwise_relation _ (pointwise_relation _ (pointwise_relation _ (⊣⊢)))
-      ==> (=) ==> (=) ==> (⊣⊢)) (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
+            ==> (=) ==> (=) ==> (⊣⊢))
+           (big_sepM2 (PROP:=PROP) (K:=K) (A:=A) (B:=B)).
   Proof. intros f g Hf m1 ? <- m2 ? <-. apply big_sepM2_proper; intros; apply Hf. Qed.
 
   (** Shows that some property [P] is closed under [big_sepM2]. Examples of [P]
@@ -2592,6 +2611,10 @@ Section gset.
   Global Instance big_sepS_mono' :
     Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepS_mono. Qed.
+  Global Instance big_sepS_flip_mono' :
+    Proper (pointwise_relation _ (flip (⊢)) ==> (=) ==> flip (⊢))
+           (big_opS (@bi_sep PROP) (A:=A)).
+  Proof. solve_proper. Qed.
 
   Global Instance big_sepS_empty_persistent Φ :
     Persistent ([∗ set] x ∈ ∅, Φ x).
@@ -2931,6 +2954,10 @@ Section gmultiset.
   Global Instance big_sepMS_mono' :
      Proper (pointwise_relation _ (⊢) ==> (=) ==> (⊢)) (big_opMS (@bi_sep PROP) (A:=A)).
   Proof. intros f g Hf m ? <-. by apply big_sepMS_mono. Qed.
+  Global Instance big_sepMS_flip_mono' :
+     Proper (pointwise_relation _ (flip (⊢)) ==> (=) ==> flip (⊢))
+            (big_opMS (@bi_sep PROP) (A:=A)).
+  Proof. solve_proper. Qed.
 
   Global Instance big_sepMS_empty_persistent Φ :
     Persistent ([∗ mset] x ∈ ∅, Φ x).
diff --git a/tests/bi.v b/tests/bi.v
index c16a6467b39e1d0fdb47c0af0993de0ac066132a..91f873f599947cc6d6c2db9aa82ddb9abde046d9 100644
--- a/tests/bi.v
+++ b/tests/bi.v
@@ -17,6 +17,20 @@ Proof.
   pose proof (bi.wand_iff_refl (PROP:=PROP) (<affine> True)).
 Abort.
 
+(** Rewriting on big ops. *)
+Goal ∀ {PROP : bi} {l : list nat} {Φ Ψ} {R : PROP},
+  (∀ k i, Φ k i ⊢ Ψ k i) → (R ⊢ [∗ list] k↦i ∈ l, Φ k i) →
+  R ⊢ [∗ list] k↦i ∈ l, Ψ k i.
+Proof. move=> > H ?. by setoid_rewrite <-H. Qed.
+Goal ∀ {PROP : bi} {m : gmap nat nat} {Φ Ψ} {R : PROP},
+  (∀ k i, Φ k i ⊢ Ψ k i) → (R ⊢ [∗ map] k↦i ∈ m, Φ k i) →
+  R ⊢ [∗ map] k↦i ∈ m, Ψ k i.
+Proof. move=> > H ?. by setoid_rewrite <-H. Qed.
+Goal ∀ {PROP : bi} {m1 m2 : gmap nat nat} {Φ Ψ} {R : PROP},
+  (∀ k i j, Φ k i j ⊢ Ψ k i j) → (R ⊢ [∗ map] k↦i;j ∈ m1;m2, Φ k i j) →
+  R ⊢ [∗ map] k↦i;j ∈ m1;m2, Ψ k i j.
+Proof. move=> > H ?. by setoid_rewrite <-H. Qed.
+
 (** Some basic tests to make sure patterns work in big ops. *)
 Definition big_sepM_pattern_value
     {PROP : bi} (m : gmap nat (nat * nat)) : PROP :=