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