From fb1028935d0e14880d850b1b833d81767e747922 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 9 Feb 2016 14:22:56 +0100
Subject: [PATCH] add a stub lemma in co_pset

---
 theories/co_pset.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/co_pset.v b/theories/co_pset.v
index 55efb4f7..7516f56c 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -332,6 +332,12 @@ Proof.
   * by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
 Qed.
 
+Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
+Proof.
+  rewrite coPset_finite_spec; simpl.
+  (* FIXME no time to finish right now, but I think it holds *)
+Abort. 
+
 (** * Splitting of infinite sets *)
 Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw :=
   match t with
-- 
GitLab