proposition: Lemma umall2_trans : Transitive P -> Transitive um_all2.
proof: Proof. by move=>T x y z H1 H2 k; apply: Transitive_optionR (H1 k) (H2 k). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)