Prove coPset_suffixes_infinite.

fff4fc98 · Robbert Krebbers · 0d5272ec · fff4fc98
Commit fff4fc98 authored Feb 09, 2016 by Robbert Krebbers
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 3 deletions

prelude/co_pset.v prelude/co_pset.v +2 -3

No files found.
--- a/prelude/co_pset.v
+++ b/prelude/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 :=