Commit fb102893 authored by Ralf Jung's avatar Ralf Jung

add a stub lemma in co_pset

parent 0ef88ec6
......@@ -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
......
Markdown is supported
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