proposition: Lemma fin_eta (fs : FinProd) : fs = finprod (sel^~ fs).
proof: Proof. by apply: fin_ext=>a; rewrite sel_fin. 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)