proposition: Lemma updi_last x v vs : updi x (rcons vs v) = updi x vs \+ x.+(size vs) :-> v.
proof: Proof. elim: vs x v=>[|w vs IH] x v /=. - by rewrite ptr0 unitR unitL. by rewrite -(addn1 (size vs)) addnC -ptrA IH joinA. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)