From dd96c209987fb7f561208c97c22cfb52c9231284 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <gitlab-sws@robbertkrebbers.nl>
Date: Mon, 6 Dec 2021 19:40:25 +0000
Subject: [PATCH] simplify proof

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

diff --git a/theories/decidable.v b/theories/decidable.v
index 22bb51f4..f149b0b2 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -192,12 +192,8 @@ Proof. case_bool_decide; intuition discriminate. Qed.
 Lemma bool_decide_iff (P Q : Prop) `{Decision P, Decision Q} :
   (P ↔ Q) → bool_decide P = bool_decide Q.
 Proof. repeat case_bool_decide; tauto. Qed.
-Lemma bool_decide_negb (P : Prop) `{Decision P} : negb (bool_decide P) = bool_decide (not P).
-Proof.
-  case_bool_decide.
-  - simpl. symmetry. apply bool_decide_eq_false. auto.
-  - simpl. symmetry. apply bool_decide_eq_true. auto.
-Qed.
+Lemma bool_decide_negb P `{Decision P} : negb (bool_decide P) = bool_decide (not P).
+Proof. repeat case_bool_decide; intuition. Qed.
 
 Lemma bool_decide_eq_true_1 P `{!Decision P}: bool_decide P = true → P.
 Proof. apply bool_decide_eq_true. Qed.
-- 
GitLab