From 1bef8f4a74193aeed094045513cda91e9ffc4b32 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 9 Feb 2016 15:02:17 +0100
Subject: [PATCH] Prove coPset_suffixes_infinite.

---
 theories/co_pset.v | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/theories/co_pset.v b/theories/co_pset.v
index 7516f56c..3b49cb37 100644
--- a/theories/co_pset.v
+++ b/theories/co_pset.v
@@ -331,12 +331,11 @@ Proof.
       rewrite ?coPset_elem_of_node; naive_solver.
   * 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. 
+  induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver.
+Qed.
 
 (** * Splitting of infinite sets *)
 Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw :=
-- 
GitLab