proposition: Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → (l = coPLeaf true → r = coPLeaf true → b = true → False) → (l = coPLeaf false → r = coPLeaf false → b = false → False) → coPset_wf (coPNode b l r).
proof: Proof. destruct b, l as [[]|], r as [[]|]; naive_solver. Qed.
imports: stdpp(pmap gmap mapset) stdpp(options)