fact: Fixpoint sel' (a : A) (xs : seq A) := if xs is x :: xs' as xs return a \in xs -> FinProd' T xs -> T a then fun pf '(f, fs) => match decP (a =P x) with left eqf => cast T eqf f | right neqf => sel' a xs' (mem_cdr pf neqf) fs end else fun pf _ => mem_nil pf.
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat seq eqtype choice fintype) pcm(options axioms) Coq(Classes.Morphisms Program.Basics Program.Tactics) Coq(Relations)