proposition: Lemma domPt A x (v : A) : dom (x :-> v) =i [pred y | (x == y) && (x != null)].
proof: Proof. move=>y; rewrite domU dom0 !inE /=. by case: ifP=>E; rewrite -(eq_sym y) E andbC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep