proposition: Lemma imfset_comp f g (p : finmempred _) : imfset key (g \o f) p = g @` (imfset key f p).
proof: Proof. apply/fsetP=> a; apply/imfsetP/imfsetP=> [[/= x xA ->]|]. by exists (f x); rewrite // in_imfset. by move=> [/= x /imfsetP [/= y yA ->] ->]; exists y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)