diff --git a/theories/decidable.v b/theories/decidable.v
index e9d3af21a9e9412a05b1112a1ad98a9b07627931..684178f5ca83046db49a76673e4a0f41a661c1fb 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -121,13 +121,9 @@ Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
 Proof. repeat case_bool_decide; tauto. Qed.
 
 Lemma bool_decide_true_2 P `{!Decision P}: bool_decide P = true → P.
-Proof. intros Heq. eapply bool_decide_unpack. rewrite Heq. exact I. Qed.
+Proof. case_bool_decide; auto || discriminate.  Qed.
 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. }
-  case_bool_decide; auto || discriminate.
-Qed.
+Proof. case_bool_decide; auto || discriminate. Qed.
 
 (** * Decidable Sigma types *)
 (** Leibniz equality on Sigma types requires the equipped proofs to be