proposition: Lemma updiVm' x m xs : m > 0 -> x \notin dom (updi x.+m xs).
proof: Proof. elim: xs x m=>[|v vs IH] x m H; first by rewrite dom0. rewrite /= ptrA domPtUn inE /= negb_and negb_or -{4}(ptr0 x) ptrK -lt0n H /=. by rewrite orbC IH // addn1. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)