fact: Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool := match t, p with | coPLeaf b, _ => b | coPNode b l r, 1 => b | coPNode _ l _, p~0 => coPset_elem_of_raw p l | coPNode _ _ r, p~1 => coPset_elem_of_raw p r end.
imports: stdpp(pmap gmap mapset) stdpp(options)