diff --git a/theories/decidable.v b/theories/decidable.v
index c3d94f5f712a94c62a6fd45f133ce86c2e6b5429..eb93b48f8b8862f934a277badfe1e66fca610c7c 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -21,7 +21,7 @@ Proof. destruct (decide P); tauto. Qed.
 Lemma decide_False {A} `{Decision P} (x y : A) :
   ¬P → (if decide P then x else y) = y.
 Proof. destruct (decide P); tauto. Qed.
-Lemma decide_iff {A} P Q `{Decision P, Decision Q} (x y : A) :
+Lemma decide_ext {A} P Q `{Decision P, Decision Q} (x y : A) :
   (P ↔ Q) → (if decide P then x else y) = (if decide Q then x else y).
 Proof. intros [??]. destruct (decide P), (decide Q); tauto. Qed.
 
@@ -189,9 +189,9 @@ Lemma bool_decide_eq_true (P : Prop) `{Decision P} : bool_decide P = true ↔ P.
 Proof. case_bool_decide; intuition discriminate. Qed.
 Lemma bool_decide_eq_false (P : Prop) `{Decision P} : bool_decide P = false ↔ ¬P.
 Proof. case_bool_decide; intuition discriminate. Qed.
-Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
+Lemma bool_decide_ext (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide Q.
-Proof. repeat case_bool_decide; tauto. Qed.
+Proof. apply decide_ext. Qed.
 
 Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
 Proof. apply bool_decide_eq_true. Qed.
diff --git a/theories/list.v b/theories/list.v
index 86256aa504757ab5f40a922f5b390e0ba1803a5c..5341d91eb7f2f5efcced2c032c7f5e7f5c0526d5 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1993,7 +1993,7 @@ Lemma list_filter_filter (P1 P2 : A → Prop)
 Proof.
   induction l as [|x l IH]; [done|].
   rewrite !filter_cons. case (decide (P2 x)) as [HP2|HP2].
-  - rewrite filter_cons, IH. apply decide_iff. naive_solver.
+  - rewrite filter_cons, IH. apply decide_ext. naive_solver.
   - rewrite IH. symmetry. apply decide_False. by intros [_ ?].
 Qed.
 
@@ -3727,7 +3727,7 @@ Section find.
     list_find P l = list_find Q l.
   Proof.
     intros HPQ. induction l as [|x l IH]; simpl; [done|].
-    by rewrite (decide_iff (P x) (Q x)), IH by done.
+    by rewrite (decide_ext (P x) (Q x)), IH by done.
   Qed.
 End find.
 
diff --git a/theories/list_numbers.v b/theories/list_numbers.v
index 53d886490424f71cbb188f6e57d2a6a1b42802d4..758f3660546ccf870fc0f64ca1c0500d825b85ff 100644
--- a/theories/list_numbers.v
+++ b/theories/list_numbers.v
@@ -340,7 +340,7 @@ Section Z_little_endian.
       by rewrite Z_ones_spec, bool_decide_true, andb_true_r by lia.
     - rewrite andb_false_r, orb_false_l.
       rewrite Z.shiftr_spec by lia. f_equal; [f_equal; lia|].
-      rewrite !Z_ones_spec by lia. apply bool_decide_iff. lia.
+      rewrite !Z_ones_spec by lia. apply bool_decide_ext. lia.
   Qed.
 
   Lemma Z_to_little_endian_length m n z :