proposition: Lemma umall2Pt2 k1 k2 v1 v2 : um_all2 (pts k1 v1) (pts k2 v2) <-> if k1 == k2 then C k1 -> P v1 v2 else ~~ C k1 && ~~ C k2.
proof: Proof. split; last first. - case: eqP=>[-> H|N /andP [C1 C2]] k. - by rewrite /optionR /= !findPt2; case: ifP=>// /andP []. by rewrite /optionR /= !findPt2 (negbTE C1) (negbTE C2) !andbF. move=>X; move: (X k1) (X k2). rewrite /optionR !findPt !findPt2 (eq_sym k2 k1) /=. case: (k1 =P k2)=>[<-|N] /=; first by case: ifP. by do 2![case: ifP]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)