fact: Definition pffun (p : {perm I}) (f : {ffun I -> A}) := [ffun i => f (p i)].
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)