proposition: Lemma updiS x v vs : updi x (v :: vs) = x :-> v :+ updi (x .+ 1) vs.
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep