proposition: Lemma defPtUn A h x (v : A) : def (x :-> v :+ h) = [&& x != null, def h & x \notin dom h].
proof: Proof. case: defUn; last 1 first. - by rewrite defPt=>H1 -> H2; rewrite H1 (H2 x) // domPt inE /= eq_refl. - by rewrite defPt; move/negbTE=>->. - by move/negbTE=>->; rewrite andbF. by move=>y; rewrite domPt inE /=; case/andP; move/eqP=><-->->; rewrite andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep