fact: Fixpoint Pset_ne_to_coPset_raw (t : Pmap_ne ()) : coPset_raw := pmap.Pmap_ne_case t $ λ ml mx mr, coPNode match mx with Some _ => true | None => false end (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw ml) (Pset_to_coPset_raw_aux Pset_ne_to_coPset_raw mr).
imports: stdpp(pmap gmap mapset) stdpp(options)