diff --git a/CHANGELOG.md b/CHANGELOG.md
index cd68a8fba8179592f6544468ea76f8729bbc098c..36c370d031dbaedddf52369d6400edaab0a1aab9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -12,6 +12,7 @@ Coq 8.10 is no longer supported by this release.
 - Add `bool_to_Z` that converts true to 1 and false to 0. (by Michael Sammler)
 - Add lemmas for lookup on `mjoin` for lists. (by Michael Sammler)
 - Rename `Is_true_false` → `Is_true_false_2` and `eq_None_ne_Some` → `eq_None_ne_Some_1`.
+- Rename `decide_iff` → `decide_ext` and `bool_decide_iff` → `bool_decide_ext`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
@@ -20,6 +21,8 @@ Note that the script is not idempotent, do not run it twice.
 sed -i -E -f- $(find theories -name "*.v") <<EOF
 s/\bIs_true_false\b/Is_true_false_2/g
 s/\beq_None_ne_Some\b/eq_None_ne_Some_1/g
+# bool decide
+s/\b(bool_|)decide_iff\b/\1decide_ext/g
 EOF
 ```
 
diff --git a/theories/decidable.v b/theories/decidable.v
index c3d94f5f712a94c62a6fd45f133ce86c2e6b5429..39ccc1b42e9d941955a04ccd9a76edd78cd98b6d 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.
@@ -203,6 +203,10 @@ Proof. apply bool_decide_eq_false. Qed.
 Lemma bool_decide_eq_false_2 P `{!Decision P}: ¬P → bool_decide P = false.
 Proof. apply bool_decide_eq_false. Qed.
 
+Lemma bool_decide_True : bool_decide True = true.
+Proof. reflexivity. Qed.
+Lemma bool_decide_False : bool_decide False = false.
+Proof. reflexivity. Qed.
 Lemma bool_decide_not P `{Decision P} :
   bool_decide (¬ P) = negb (bool_decide P).
 Proof. repeat case_bool_decide; intuition. Qed.
@@ -212,6 +216,12 @@ Proof. repeat case_bool_decide; intuition. Qed.
 Lemma bool_decide_and P Q `{Decision P, Decision Q} :
   bool_decide (P ∧ Q) = bool_decide P && bool_decide Q.
 Proof. repeat case_bool_decide; intuition. Qed.
+Lemma bool_decide_impl P Q `{Decision P, Decision Q} :
+  bool_decide (P → Q) = implb (bool_decide P) (bool_decide Q).
+Proof. repeat case_bool_decide; intuition. Qed.
+Lemma bool_decide_iff P Q `{Decision P, Decision Q} :
+  bool_decide (P ↔ Q) = eqb (bool_decide P) (bool_decide Q).
+Proof. repeat case_bool_decide; intuition. Qed.
 
 (** The tactic [compute_done] solves the following kinds of goals:
 - Goals [P] where [Decidable P] can be derived.
diff --git a/theories/list.v b/theories/list.v
index f511a531cc409bd337d69f0a44fa0dab6824c98e..b73ac068bf9542e1a4eec264ea44aa630ec0732b 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1990,7 +1990,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.
 
@@ -3724,7 +3724,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 :