proposition: Lemma updiVm x m xs : x \in dom (updi x.+m xs) = [&& x != null, m == 0 & size xs > 0].
proof: Proof. case: m=>[|m] /=; last first. - by rewrite andbF; apply/negbTE/updiVm'. case: xs=>[|v xs]; rewrite ptr0 ?andbF ?andbT ?dom0 //=. by rewrite domPtUn inE /= eq_refl -updiS updiD orbF andbT /=. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)