diff --git a/theories/list.v b/theories/list.v
index b853eb946bc5e14d7f2ac9af444a56f75691652a..994917a015971bf5e132d317202d0044d19092e5 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -920,10 +920,8 @@ Section find.
(∀ x, P x ↔ Q x) →
list_find P l = list_find Q l.
Proof.
- intros HPQ. induction l as [|x l IH]; [done|]. simpl.
- rewrite !decide_bool_decide.
- rewrite (bool_decide_iff _ (Q x)) by done.
- rewrite IH. done.
+ intros HPQ. induction l as [|x l IH]; simpl; [done|].
+ by rewrite (decide_iff (P x) (Q x)), IH by done.
Qed.
End find.