proposition: Lemma updi_inv x xs1 xs2 : def (updi x xs1) -> updi x xs1 = updi x xs2 -> xs1 = xs2.
proof: Proof. elim: xs1 x xs2 =>[|v1 xs1 IH] x /=; case=>[|v2 xs2 D] //=; try by move/esym; rewrite empbE empUn empPt. by case/(cancel D)=><- /IH E /E->. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep