proposition: Lemma updi_catI x y vs1 vs2 : y = x.+(size vs1) -> updi x vs1 :+ updi y vs2 = updi x (vs1 ++ vs2).
proof: Proof. by move=>->; rewrite updi_cat. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep