proposition: Lemma valid_selUn (T : finType) (Us : T -> pcm) tag (x1 x2 : FinProd Us) : valid (x1 \+ x2) -> valid (sel tag x1 \+ sel tag x2).
proof: Proof. by move/forallP/(_ tag); rewrite sel_fin. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)