proposition: Lemma pffunEM (p p' : {perm I}) (f : {ffun I -> A}) : pffun (p * p') f = pffun p (pffun p' f).
proof: Proof. by apply/ffunP => i; rewrite !ffunE permM. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)