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 un0h. by rewrite -(addn1 (size vs1)) addnC -ptrA IH unA. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep