proposition: Lemma valid_finUn (T : finType) (Us : T -> pcm) (f1 f2 : forall x, Us x) : (forall t, valid (f1 t \+ f2 t)) -> valid (finprod f1 \+ finprod f2).
proof: Proof. by move=>H; apply/forallP=>x; rewrite !sel_fin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)