From 46e116b93361ab1533926e806d2922361c016417 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 30 Nov 2018 11:48:30 +0100
Subject: [PATCH] Relation between `set_seq` and `seq`.

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

diff --git a/theories/sets.v b/theories/sets.v
index 8b6d5768..23b28cf5 100644
--- a/theories/sets.v
+++ b/theories/sets.v
@@ -1086,6 +1086,10 @@ Section set_seq.
   Lemma set_seq_S_end_union_L `{!LeibnizEquiv C} start len :
     set_seq start (S len) =@{C} {[ start + len ]} ∪ set_seq start len.
   Proof. unfold_leibniz. apply set_seq_S_end_union. Qed.
+
+  Lemma list_to_set_seq start len :
+    list_to_set (seq start len) =@{C} set_seq start len.
+  Proof. revert start; induction len; intros; f_equal/=; auto. Qed.
 End set_seq.
 
 (** Mimimal elements *)
-- 
GitLab