proposition: Lemma emp_pick h : (pick h == null) = (~~ def h || empb h).
proof: Proof. case: h=>[|h] //=; case: (supp h)=>[|x xs] //=. by rewrite inE negb_or eq_sym; case/andP; move/negbTE=>->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep