fact: Fixpoint coPset_wf (t : coPset_raw) : bool := match t with | coPLeaf _ => true | coPNode true (coPLeaf true) (coPLeaf true) => false | coPNode false (coPLeaf false) (coPLeaf false) => false | coPNode _ l r => coPset_wf l && coPset_wf r end.
imports: stdpp(pmap gmap mapset) stdpp(options)