proposition: Lemma sel_spliceE fs a ta : sel a (splice fs ta) = ta.
proof: Proof. by rewrite sel_fin; case: decP=>// pf; rewrite eqc. Qed.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)