Commit 680ce446 authored by Ralf Jung's avatar Ralf Jung
Browse files

add a stub lemma in co_pset

parent fa9b9d1b
......@@ -332,6 +332,12 @@ Proof.
* by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node.
Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
rewrite coPset_finite_spec; simpl.
(* FIXME no time to finish right now, but I think it holds *)
(** * Splitting of infinite sets *)
Fixpoint coPset_l_raw (t : coPset_raw) : coPset_raw :=
match t with
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment