proposition: Lemma splice_eta fs a : splice fs (sel a fs) = fs.
proof: Proof. apply: fin_ext=>x; rewrite sel_fin. by case: decP=>// ?; subst x; 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)