proposition: Lemma spliceUn (T : finType) (Us : T -> pcm) (tag : T) (x y : FinProd Us) v w : splice (x \+ y) tag (v \+ w) = splice x tag v \+ splice y tag w.
proof: Proof. apply: fin_ext=>a; rewrite !sel_fin; case: decP=>// ?. by subst a; rewrite !eqc. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq bigop fintype finset) pcm(options axioms prelude seqperm pred seqext)