proposition: Lemma coPset_elem_of_singleton p q : e_of p (coPset_singleton_raw q) ↔ p = q.
proof: Proof. split; [|by intros <-; induction p; simpl; rewrite ?coPset_elem_of_node]. by revert q; induction p; intros [?|?|]; simpl; rewrite ?coPset_elem_of_node; intros; f_equal/=; auto. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)