diff --git a/theories/decidable.v b/theories/decidable.v
index 925a6b8644c0a87b2b04922b56ba48c7bf5ddb14..c5db311f9cb8567133e78c9d078b23c4be6adc65 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -94,6 +94,9 @@ Proof. unfold bool_decide. destruct dec; [left|right]; assumption. Qed.
Lemma bool_decide_decide P `{!Decision P} :
bool_decide P = if decide P then true else false.
Proof. reflexivity. Qed.
+Lemma decide_bool_decide P {Hdec: Decision P} {X : Type} (x1 x2 : X):
+ (if decide P then x1 else x2) = (if bool_decide P then x1 else x2).
+Proof. unfold bool_decide, decide. destruct Hdec; reflexivity. Qed.
Tactic Notation "case_bool_decide" "as" ident (Hd) :=
match goal with
diff --git a/theories/list.v b/theories/list.v
index f79766d514b27a067b255f96b56ca099c1355e9b..b853eb946bc5e14d7f2ac9af444a56f75691652a 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -921,7 +921,9 @@ Section find.
list_find P l = list_find Q l.
Proof.
intros HPQ. induction l as [|x l IH]; [done|]. simpl.
- erewrite decide_iff by done. by rewrite IH.
+ rewrite !decide_bool_decide.
+ rewrite (bool_decide_iff _ (Q x)) by done.
+ rewrite IH. done.
Qed.
End find.