proposition: Lemma umall2fUn f f1 f2 : Reflexive P -> valid f1 = valid f2 -> um_all2 f1 f2 -> um_all2 (f \+ f1) (f \+ f2).
proof: Proof. move=>R Ev X; have De : dom_eq f1 f2. - by apply/domeqP; rewrite (umall2_dom X) Ev. move=>k; case V1 : (valid (f \+ f1)) (domeqVUnE (domeq_refl f) De)=>/esym V2; last first. - by move/negbT/invalidE: V1 V2=>-> /negbT/invalidE ->; rewrite find_undef. rewrite /optionR /= !findUnL //; case: ifP=>D; last by apply: X. by case/In_domX: D=>v /In_find ->; apply: R. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)