proposition: Lemma domPtUn A h x (v : A) : dom (x :-> v :+ h) =i [pred y | def (x :-> v :+ h) && ((x == y) || (y \in dom h))].
proof: Proof. move=>y; rewrite domUn !inE !defPtUn domPt inE /=. by case: (x =P null)=>//= _; rewrite andbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep