proposition: Lemma umall2KL f1 f2 g1 g2 : Equivalence_rel P -> valid (f1 \+ g1) -> valid (f2 \+ g2) -> um_all2 (f1 \+ g1) (f2 \+ g2) -> um_all2 f1 f2 -> um_all2 g1 g2.
proof: Proof. move=>E; case/Equivalence_relS: E=>R S T. move=>V1 V2 H1 Ha; have /(umall2_sym S) H2: um_all2 (f1 \+ g1) (f2 \+ g1). - by apply: umall2Unf Ha=>//; rewrite (validL V1) (validL V2). apply: umall2fK (V2) _; last first. - by apply: umall2_trans H2 H1. apply: domeqVUn (V1)=>//; apply/domeqP. by rewrite (validL V1) (validL V2) (umall2_dom Ha). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)