fact: Fixpoint coPpick_raw (t : coPset_raw) : option positive := match t with | coPLeaf true | coPNode true _ _ => Some 1 | coPLeaf false => None | coPNode false l r => match coPpick_raw l with | Some i => Some (i~0) | None => (~1) <$> coPpick_raw r end end.
imports: stdpp(pmap gmap mapset) stdpp(options)