fact: Definition indx {I : finType} (x : I) := index x (enum I).
imports: Coq(ssreflect ssrbool ssrfun Eqdep) mathcomp(ssrnat eqtype seq path) pcm(options axioms finmap) pcm(pcm unionmap) mathcomp(fintype tuple finfun)