proposition: Lemma elem_coPset_suffixes p q : p ∈ coPset_suffixes q ↔ ∃ q', p = q' ++ q.
proof: Proof. unfold elem_of, coPset_elem_of; simpl; split. - revert p; induction q; intros [?|?|]; simpl; rewrite ?coPset_elem_of_node; naive_solver. - by intros [q' ->]; induction q; simpl; rewrite ?coPset_elem_of_node. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)