fact: Definition inE := (inE, mem_codomf, mem_catf, mem_remfF, mem_filterf, mem_reducef, mem_restrictf, mem_remf, mem_remf1, mem_setf).
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)