proposition: Lemma elem_of_Pset_to_coPset_raw i t : e_of i (Pset_to_coPset_raw t) ↔ t !! i = Some ().
proof: Proof. revert i. induction t as [|ml mx mr] using pmap.Pmap_ind; [done|]. intros []; rewrite Pset_to_coPset_raw_PNode, pmap.Pmap_lookup_PNode by done; destruct mx as [[]|]; naive_solver. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)