proposition: Lemma Pset_to_coPset_raw_wf t : coPset_wf (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. apply coPNode_wf; [done|done|..]; destruct mx; destruct ml using pmap.Pmap_ind; destruct mr using pmap.Pmap_ind; rewrite ?Pset_to_coPset_raw_PNode by done; naive_solver. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)