proposition: Lemma updimV x m xs : x.+m \in dom (updi x xs) = (x != null) && (m < size xs).
proof: Proof. case H: (x == null)=>/=. - case: xs=>[|a s]; first by rewrite dom0. by rewrite domPtUn inE validPtUn /= H. elim: xs x m H=>[|v vs IH] x m H //; case: m=>[|m]; try by rewrite /= dom0. - by rewrite ptr0 domPtUn inE /= eq_refl andbT -updiS updiD H. rewrite -addn1 addnC -ptrA updiS domPtUn inE /= IH; last first. - by rewrite ptrE /= addn1. by rewrite -updiS updiD H /= -{1}(ptr0 x) ptrA ptrK. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)