From d4b57ae83e63eb9624db7e346909b57efa52ad0e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Tue, 27 Mar 2018 16:19:45 +0200
Subject: [PATCH] Add `seq_set_start_disjoint`
---
theories/collections.v | 4 ++++
1 file changed, 4 insertions(+)
diff --git a/theories/collections.v b/theories/collections.v
index a650917f..31c971ee 100644
--- a/theories/collections.v
+++ b/theories/collections.v
@@ -1053,6 +1053,10 @@ Section seq_set.
- rewrite elem_of_union, elem_of_singleton, IH. omega.
Qed.
+ Lemma seq_set_start_disjoint start len :
+ {[ start ]} ## seq_set (C:=C) (S start) len.
+ Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
+
Lemma seq_set_S_disjoint start len :
{[ start + len ]} ## seq_set (C:=C) start len.
Proof. intros x. rewrite elem_of_singleton, elem_of_seq_set. omega. Qed.
--
GitLab