proposition: Lemma umall2cancel k v1 v2 f1 f2 : valid (pts k v1 \+ f1) -> valid (pts k v2 \+ f2) -> um_all2 (pts k v1 \+ f1) (pts k v2 \+ f2) -> P v1 v2 /\ um_all2 f1 f2.
proof: Proof. move=>V1 V2 X; split=>[|x]. - by move: (X k); rewrite !findPtUn. move: (X x); rewrite !findPtUn2 //; case: ifP=>// /eqP -> _. by case: dom_find (validPtUnD V1)=>// ->; case: dom_find (validPtUnD V2)=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)