proposition: Lemma updi_inv x xs1 xs2 : valid (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; [move/esym| |]; try by rewrite unitbE um_unitbUn um_unitbPt. by case/(hcancelV D)=><- {}D /(IH _ _ D) <-. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)