From 89a5e9bc280a48e2a05de6e17bf9df65578710c0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sun, 30 Jun 2019 18:58:12 +0200
Subject: [PATCH] simplify proofs even more

---
 theories/decidable.v | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/theories/decidable.v b/theories/decidable.v
index e9d3af21..684178f5 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
-- 
GitLab