proposition: Lemma finprod_beta' (f : forall x, T x) a xs : forall pf : a \in xs, sel' pf (finprod' xs f) = f a.
proof: Proof. by elim: xs=>[|x xs IH] //= pf; case: decP=>// {}pf; 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)