proposition: Lemma Pset_to_coPset_raw_finite t : coPset_finite (Pset_to_coPset_raw t).
proof: Proof. induction t as [|ml mx mr] using pmap.Pmap_ind; [done|]. rewrite Pset_to_coPset_raw_PNode by done. destruct mx; naive_solver. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)