proposition: Lemma defU h x d : def (upd h x d) = (x != null) && (def h).
proof: Proof. case: h=>[|h H] /=; first by rewrite andbF. by rewrite /upd; case: decP=>/= [->//|]; case: eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep