proposition: Lemma sel_fin f a : sel a (finprod f) = f a.
proof: Proof. by rewrite /sel finprod_beta'. 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)