proposition: Lemma umcompfUn g f1 f2 : valid (f1 \+ f2) -> um_comp g (f1 \+ f2) = um_comp g f1 \+ um_comp g f2.
proof: Proof. rewrite /um_comp=>W; rewrite umfoldlUn_frame ?unitR //. by move=>*; case: (find _ _)=>// a; rewrite joinA. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)