proposition: Lemma coPset_suffixes_infinite p : ¬set_finite (coPset_suffixes p).
proof: Proof. rewrite coPset_finite_spec; simpl. induction p; simpl; rewrite ?coPset_finite_node, ?andb_True; naive_solver. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)