proposition: Lemma defUnhh h : def (h :+ h) = empb h.
proof: Proof. case E: (empb h); first by move/empbE: E=>->. case: defUn=>// D _ L. case: defE E=>//; case; split=>// x. case E: (x \in dom h)=>//. by move: (L x E); rewrite E. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep