fact: Fixpoint coPset_r_raw (t : coPset_raw) : coPset_raw := match t with | coPLeaf false => coPLeaf false | coPLeaf true => coPNode false (coPLeaf false) (coPLeaf true) | coPNode b l r => coPNode' false (coPset_r_raw l) (coPset_r_raw r) end.
imports: stdpp(pmap gmap mapset) stdpp(options)