From 5bb9627f73d54346bef7c0df038fb0ac2be1b6bd Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 1 Jun 2021 16:56:43 +0200
Subject: [PATCH] =?UTF-8?q?Make=20`elem=5Fof=5FPermutation`=20a=20`?=
 =?UTF-8?q?=E2=86=94`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

diff --git a/theories/list.v b/theories/list.v
index f2d9a5d0..b1cc30e7 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1753,8 +1753,12 @@ Proof.
   revert i; induction l as [|y l IH]; intros [|i] ?; simplify_eq/=; auto.
   by rewrite Permutation_swap, <-(IH i).
 Qed.
-Lemma elem_of_Permutation l x : x ∈ l → ∃ k, l ≡ₚ x :: k.
-Proof. intros [i ?]%elem_of_list_lookup. eauto using delete_Permutation. Qed.
+Lemma elem_of_Permutation l x : x ∈ l ↔ ∃ k, l ≡ₚ x :: k.
+Proof.
+  split.
+  - intros [i ?]%elem_of_list_lookup. eexists. by apply delete_Permutation.
+  - intros [k ->]. by left.
+Qed.
 
 Lemma Permutation_cons_inv l k x :
   k ≡ₚ x :: l → ∃ k1 k2, k = k1 ++ x :: k2 ∧ l ≡ₚ k1 ++ k2.
-- 
GitLab