proposition: Lemma umall2Pt k v1 v2 : C k -> um_all2 (pts k v1) (pts k v2) <-> P v1 v2.
proof: Proof. by move=>C'; rewrite umall2Pt2 eq_refl; split=>//; apply. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)