From c1687739d086a13d296083010f0e295b084c8880 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Feb 2017 17:37:10 +0100
Subject: [PATCH] Prove elem_of_submseteq.

---
 theories/list.v | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/theories/list.v b/theories/list.v
index 6c25da83..2de2b7b5 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -1873,6 +1873,10 @@ Proof.
 Qed.
 Global Instance: AntiSymm (≡ₚ) (@submseteq A).
 Proof. red. auto using submseteq_Permutation_length_le, submseteq_length. Qed.
+
+Lemma elem_of_submseteq l k x : x ∈ l → l ⊆+ k → x ∈ k.
+Proof. intros ? [l' ->]%submseteq_Permutation. apply elem_of_app; auto. Qed.
+
 Lemma submseteq_take l i : take i l ⊆+ l.
 Proof. auto using sublist_take, sublist_submseteq. Qed.
 Lemma submseteq_drop l i : drop i l ⊆+ l.
-- 
GitLab