proposition: Lemma pickP h : valid h && ~~ unitb h = (pick h \in dom h).
proof: Proof. rewrite /dom /unitb /= /empb pcmE; case: h=>[|h] //=. by case: (supp h)=>// *; rewrite inE eq_refl. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)