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