diff --git a/theories/decidable.v b/theories/decidable.v
index ddb90db6885227aaaca4a59493ea060b59cc7872..e9d3af21a9e9412a05b1112a1ad98a9b07627931 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -126,7 +126,7 @@ Lemma bool_decide_false_2 P `{!Decision P}: bool_decide P = false → ¬P.
 Proof.
   intros Heq HP. assert (HP': bool_decide P).
   { apply bool_decide_spec. assumption. }
-  destruct (bool_decide P). discriminate. contradiction.
+  case_bool_decide; auto || discriminate.
 Qed.
 
 (** * Decidable Sigma types *)