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