fact: Definition fun_of_fin ph (f : finfun_of ph) x := let: FinfunOf f_aT := f in fun_of_fin_rec f_aT (mem_enum aT x).
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple)