fact: Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw := match b, l, r with | true, coPLeaf true, coPLeaf true => coPLeaf true | false, coPLeaf false, coPLeaf false => coPLeaf false | _, _, _ => coPNode b l r end.
imports: stdpp(pmap gmap mapset) stdpp(options)