diff --git a/CHANGELOG.md b/CHANGELOG.md
index 5a18b3456fe6a1dd09adf332d618850a49849442..deec3e67a689e01d2ffa3f21c3b21c28ed928168 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -42,6 +42,7 @@ API-breaking change is listed.
 - Add function `kmap` to transform the keys of finite maps.
 - Set `Hint Mode` for the classes `PartialOrder`, `TotalOrder`, `MRet`, `MBind`,
   `MJoin`, `FMap`, `OMap`, `MGuard`, `SemiSet`, `Set_`, `TopSet`, and `Infinite`.
+- Make `map_filter_strong_ext` and `map_filter_ext` bidirectional.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 473196e0d3ee5d36d97bf75b1883e1e16e6a773f..2b568bfca9a603ed28df8c8a92d8789dc6dffa2c 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -1326,16 +1326,24 @@ Section map_filter_ext.
   Context {A} (P Q : K * A → Prop) `{!∀ x, Decision (P x), !∀ x, Decision (Q x)}.
 
   Lemma map_filter_strong_ext (m1 m2 : M A) :
-    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) →
-    filter P m1 = filter Q m2.
+    filter P m1 = filter Q m2 ↔
+    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)).
   Proof.
-    intros HPiff. apply map_eq. intros i. apply option_eq; intros x.
-    rewrite !map_filter_lookup_Some. naive_solver.
+    intros. rewrite map_eq_iff. setoid_rewrite option_eq.
+    setoid_rewrite map_filter_lookup_Some. naive_solver.
   Qed.
+  Lemma map_filter_strong_ext_1 (m1 m2 : M A) :
+    (∀ i x, (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x)) →
+    filter P m1 = filter Q m2.
+  Proof. by rewrite map_filter_strong_ext. Qed.
+  Lemma map_filter_strong_ext_2 (m1 m2 : M A) i x :
+    filter P m1 = filter Q m2 →
+    (P (i, x) ∧ m1 !! i = Some x) ↔ (Q (i, x) ∧ m2 !! i = Some x).
+  Proof. by rewrite map_filter_strong_ext. Qed.
   Lemma map_filter_ext (m : M A) :
-    (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) →
+    (∀ i x, m !! i = Some x → P (i, x) ↔ Q (i, x)) ↔
     filter P m = filter Q m.
-  Proof. intro. apply map_filter_strong_ext. naive_solver. Qed.
+  Proof. rewrite map_filter_strong_ext. naive_solver. Qed.
 End map_filter_ext.
 
 Section map_filter_insert_and_delete.