proposition: Lemma updiP x y xs : reflect (y != null /\ exists m, x = y.+m /\ m < size xs) (x \in dom (updi y xs)).
proof: Proof. case H: (y == null)=>/=. - rewrite (eqP H); elim: xs=>[|z xs IH]. - by rewrite dom0; constructor; case. by rewrite domPtUn inE validPtUn; constructor; case. case E: (x \in _); constructor; last first. - by move=>[_][m][H1] H2; rewrite H1 updimV H2 H in E. case: (ptrT x y) E=>m; case/orP; move/eqP=>->. - by rewrite updimV H /= => H1; split=>//; exists m. rewrite updiVm; case/and3P=>H1; move/eqP=>-> H2. by split=>//; exists 0; rewrite ptrA addn0 ptr0. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)