proposition: Lemma updiD x xs : def (updi x xs) = (x != null) || (size xs == 0).
proof: Proof. elim: xs x=>[|v xs IH] x //=; first by rewrite orbC. by rewrite defPtUn updiVm' // orbF IH ptr_null andbF andbC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep