proposition: Lemma updi_iinv x xs1 xs2 h1 h2 : size xs1 = size xs2 -> valid (updi x xs1 \+ h1) -> updi x xs1 \+ h1 = updi x xs2 \+ h2 -> xs1 = xs2 /\ h1 = h2.
proof: Proof. elim: xs1 x xs2 h1 h2=>[|v1 xs1 IH] x /=; case=>[|v2 xs2] //= h1 h2. - by rewrite !unitL. move=>[E]; rewrite -!joinA=>D; case/(hcancelV D)=><-{}D. by case/(IH _ _ _ _ E D)=>->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap)