proposition: Lemma lookPtUn A h x (v : A) : def (x :-> v :+ h) -> look x (x :-> v :+ h) = dyn v.
proof: Proof. by move=>D; rewrite lookUnl // lookU domPt !inE eq_refl (defPt_null D). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep