Commit 1bef8f4a authored by Robbert Krebbers's avatar Robbert Krebbers

Prove coPset_suffixes_infinite.

parent fb102893
......@@ -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 :=
......
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