proposition: Lemma umall2_eq : Equivalence_rel P -> Equivalence_rel um_all2.
proof: Proof. case/Equivalence_relS=>R S T; apply/Equivalence_relS; split. - by move=>f; apply: umall2_refl. - by apply: umall2_sym. by apply: umall2_trans. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)