proposition: Lemma updiD x xs : valid (updi x xs) = (x != null) || (size xs == 0).
proof: Proof. elim: xs x=>[|v xs IH] x; first by rewrite valid_unit orbC. by rewrite validPtUn updiVm' // orbF IH ptr_null andbF andbC. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)