From 3eb9d4894154f0ce902a442fb04c6c5bd282f7ac Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 Jul 2019 20:37:02 +0200
Subject: [PATCH] Simplify proof of `list_find_ext`.
---
theories/list.v | 6 ++----
1 file changed, 2 insertions(+), 4 deletions(-)
diff --git a/theories/list.v b/theories/list.v
index b853eb94..994917a0 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.
--
GitLab