proposition: Lemma upd_inj h x d1 d2 : def h -> x != null -> upd h x d1 = upd h x d2 -> d1 = d2.
proof: Proof. case: h=>[|h H] // _ H1; rewrite /upd; case: decP=>// H2 [E]. have: fnd x (ins x d1 h) = fnd x (ins x d2 h) by rewrite E. by rewrite !fnd_ins eq_refl; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep