diff --git a/algebra/auth.v b/algebra/auth.v
index d2311b0d59ff48cb5be48bfefffadc54bbce00c4..daa508e25748c0430c3de1279986979ead6441fd 100644
--- a/algebra/auth.v
+++ b/algebra/auth.v
@@ -275,7 +275,7 @@ Lemma auth_map_ext {A B : ofeT} (f g : A → B) x :
   (∀ x, f x ≡ g x) → auth_map f x ≡ auth_map g x.
 Proof.
   constructor; simpl; auto.
-  apply option_fmap_setoid_ext=> a; by apply excl_map_ext.
+  apply option_fmap_equiv_ext=> a; by apply excl_map_ext.
 Qed.
 Instance auth_map_ne {A B : ofeT} n :
   Proper ((dist n ==> dist n) ==> dist n ==> dist n) (@auth_map A B).
diff --git a/algebra/cmra.v b/algebra/cmra.v
index 08117babe892f8415e2de5af006af85c64eb21a0..f75552747da6b23029bdb61df6bb70ab25d520f3 100644
--- a/algebra/cmra.v
+++ b/algebra/cmra.v
@@ -1250,11 +1250,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply rFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply rFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply rFunctor_compose.
 Qed.
 
 Instance optionURF_contractive F :
diff --git a/algebra/gmap.v b/algebra/gmap.v
index 0734d5c0f88198de0b1600607aec44a7286989f4..e6e4d23a8f2ac867cfd753fbe5b7deee608b3cb8 100644
--- a/algebra/gmap.v
+++ b/algebra/gmap.v
@@ -475,11 +475,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply cFunctor_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply cFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply cFunctor_compose.
 Qed.
 Instance gmapCF_contractive K `{Countable K} F :
   cFunctorContractive F → cFunctorContractive (gmapCF K F).
@@ -496,11 +496,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros K ?? F A B x. rewrite /= -{2}(map_fmap_id x).
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_id.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_id.
 Qed.
 Next Obligation.
   intros K ?? F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -map_fmap_compose.
-  apply map_fmap_setoid_ext=>y ??; apply rFunctor_compose.
+  apply map_fmap_equiv_ext=>y ??; apply rFunctor_compose.
 Qed.
 Instance gmapRF_contractive K `{Countable K} F :
   rFunctorContractive F → urFunctorContractive (gmapURF K F).
diff --git a/algebra/list.v b/algebra/list.v
index 5fd0616e8d8a5fe2b1d08665915a36b62d1c6ec6..9fca913634bc6c90bfb01f2dde0714c5c59b4d80 100644
--- a/algebra/list.v
+++ b/algebra/list.v
@@ -108,11 +108,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply cFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply cFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply cFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance listCF_contractive F :
@@ -452,11 +452,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(list_fmap_id x).
-  apply list_fmap_setoid_ext=>y. apply urFunctor_id.
+  apply list_fmap_equiv_ext=>y. apply urFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
-  apply list_fmap_setoid_ext=>y; apply urFunctor_compose.
+  apply list_fmap_equiv_ext=>y; apply urFunctor_compose.
 Qed.
 
 Instance listURF_contractive F :
diff --git a/algebra/ofe.v b/algebra/ofe.v
index a24756ca26e81fc5d684b5dbf242f7cfbc39ad85..0e59c67278a40cf60c3b5b3cb321cca93b454e50 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -820,11 +820,11 @@ Next Obligation.
 Qed.
 Next Obligation.
   intros F A B x. rewrite /= -{2}(option_fmap_id x).
-  apply option_fmap_setoid_ext=>y; apply cFunctor_id.
+  apply option_fmap_equiv_ext=>y; apply cFunctor_id.
 Qed.
 Next Obligation.
   intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -option_fmap_compose.
-  apply option_fmap_setoid_ext=>y; apply cFunctor_compose.
+  apply option_fmap_equiv_ext=>y; apply cFunctor_compose.
 Qed.
 
 Instance optionCF_contractive F :
diff --git a/prelude/fin_maps.v b/prelude/fin_maps.v
index 91b8aebb7605bf7c7cd580b36109dcadf04a06e9..34006bcb608d7b546712c6cb9a794ea30c9ea681 100644
--- a/prelude/fin_maps.v
+++ b/prelude/fin_maps.v
@@ -556,7 +556,7 @@ Proof. apply map_eq; intros i; by rewrite lookup_fmap, option_fmap_id. Qed.
 Lemma map_fmap_compose {A B C} (f : A → B) (g : B → C) (m : M A) :
   g ∘ f <$> m = g <$> f <$> m.
 Proof. apply map_eq; intros i; by rewrite !lookup_fmap,option_fmap_compose. Qed.
-Lemma map_fmap_setoid_ext `{Equiv A, Equiv B} (f1 f2 : A → B) m :
+Lemma map_fmap_equiv_ext `{Equiv A, Equiv B} (f1 f2 : A → B) m :
   (∀ i x, m !! i = Some x → f1 x ≡ f2 x) → f1 <$> m ≡ f2 <$> m.
 Proof.
   intros Hi i; rewrite !lookup_fmap.
diff --git a/prelude/list.v b/prelude/list.v
index 72cd5c6a9b108e3a76b60a13eeaadf4e7ad0e36b..dbd6e73b72a1712d6021d8eb075357c890bc3239 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -2802,7 +2802,7 @@ Section fmap.
   Lemma list_fmap_ext (g : A → B) (l1 l2 : list A) :
     (∀ x, f x = g x) → l1 = l2 → fmap f l1 = fmap g l2.
   Proof. intros ? <-. induction l1; f_equal/=; auto. Qed.
-  Lemma list_fmap_setoid_ext `{Equiv B} (g : A → B) l :
+  Lemma list_fmap_equiv_ext `{Equiv B} (g : A → B) l :
     (∀ x, f x ≡ g x) → f <$> l ≡ g <$> l.
   Proof. induction l; constructor; auto. Qed.
 
diff --git a/prelude/option.v b/prelude/option.v
index 24544dabf150910ff59137c184c79e6d889084ee..c045491ca67bf860d31e3aa9dffcd236c67afeed 100644
--- a/prelude/option.v
+++ b/prelude/option.v
@@ -180,7 +180,7 @@ Proof. unfold is_Some; destruct mx; naive_solver. Qed.
 Lemma fmap_Some {A B} (f : A → B) mx y :
   f <$> mx = Some y ↔ ∃ x, mx = Some x ∧ y = f x.
 Proof. destruct mx; naive_solver. Qed.
-Lemma fmap_Some_setoid {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
+Lemma fmap_Some_equiv {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
       (f : A → B) mx y :
   f <$> mx ≡ Some y ↔ ∃ x, mx = Some x ∧ y ≡ f x.
 Proof.
@@ -190,6 +190,10 @@ Proof.
   - intros ?%symmetry%equiv_None. done.
   - intros (? & ? & ?). done.
 Qed.
+Lemma fmap_Some_equiv' {A B} `{Equiv B} `{!Equivalence ((≡) : relation B)}
+      (f : A → B) mx y :
+  f <$> mx ≡ Some y → ∃ x, mx = Some x ∧ y ≡ f x.
+Proof. intros. apply fmap_Some_equiv. done. Qed.
 Lemma fmap_None {A B} (f : A → B) mx : f <$> mx = None ↔ mx = None.
 Proof. by destruct mx. Qed.
 Lemma option_fmap_id {A} (mx : option A) : id <$> mx = mx.
@@ -200,7 +204,7 @@ Proof. by destruct mx. Qed.
 Lemma option_fmap_ext {A B} (f g : A → B) mx :
   (∀ x, f x = g x) → f <$> mx = g <$> mx.
 Proof. intros; destruct mx; f_equal/=; auto. Qed.
-Lemma option_fmap_setoid_ext `{Equiv A, Equiv B} (f g : A → B) mx :
+Lemma option_fmap_equiv_ext `{Equiv A, Equiv B} (f g : A → B) mx :
   (∀ x, f x ≡ g x) → f <$> mx ≡ g <$> mx.
 Proof. destruct mx; constructor; auto. Qed.
 Lemma option_fmap_bind {A B C} (f : A → B) (g : B → option C) mx :