proposition: Lemma empU h x d : empb (upd h x d) = false.
proof: Proof. case: h=>[|h H] //; rewrite /upd /empb; case: decP=>// H1. suff: x \in supp (ins x d h) by case: (supp _). by rewrite supp_ins inE /= eq_refl. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep