proposition: Lemma unit_pick (h : heap) : (pick h == null) = (~~ valid h || unitb h).
proof: Proof. rewrite /unitb /= /empb !pcmE; case: h=>[|h] //=; case: (supp h)=>[|x xs] //=. by rewrite inE negb_or eq_sym; case/andP; move/negbTE=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)