proposition: Lemma sel_spliceN fs a b (tb : T b) : a <> b -> sel a (splice fs tb) = sel a fs.
proof: Proof. by move=>N; rewrite sel_fin; case: decP. 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)