proposition: Lemma umallUn f1 f2 : um_all f1 -> um_all f2 -> um_all (f1 \+ f2).
proof: Proof. by move=>X Y k v /InUn [/X|/Y]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)