proposition: Lemma umall2fK f f1 f2 : valid (f \+ f1) -> valid (f \+ f2) -> um_all2 (f \+ f1) (f \+ f2) -> um_all2 f1 f2.
proof: Proof. move=>V1 V2 X k; move: (X k); rewrite !findUnL //; case: ifP=>// D _. by case: dom_find (dom_inNL V1 D)=>// ->; case: dom_find (dom_inNL V2 D)=>// ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)