proposition: Lemma defPt A x (v : A) : def (x :-> v) = (x != null).
proof: Proof. by rewrite defU andbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep