proposition: Lemma defPt_null A h x (v : A) : def (x :-> v :+ h) -> x != null.
proof: Proof. by rewrite defPtUn; case/and3P. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep