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