proposition: Lemma valid_fin (T : finType) (Us : T -> pcm) (f : forall x, Us x) : (forall t, valid (f t)) -> valid (finprod f).
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)