proposition: Lemma umallbUn p f1 f2 : valid (f1 \+ f2) -> um_allb p (f1 \+ f2) = um_allb p f1 && um_allb p f2.
proof: Proof. move=>W; apply/idP/idP. - by move/umallbP=>H; apply/andP; split; apply/umallbP=>x X; apply: H; [apply: InL | apply: InR]. clear W. case/andP=>/umallbP X1 /umallbP X2; apply/umallbP=>x. by case/InUn; [apply: X1 | apply: X2]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path bigop) pcm(options prelude finmap seqperm pred seqext) pcm(pcm morphism)