proposition: Lemma codomf_restrict f (A : {fset K}) : codomf f.[& A] = [fset f k | k : domf f & val k \in A].
proof: Proof. apply/fsetP=> v; apply/imfsetP/imfsetP => /= [] [k kP ->]. have := valP k; rewrite inE => /andP [kf kA]; exists [` kf] => //. by rewrite !ffunE; apply: eq_getf. have kA : val k \in [fset x | x in domf f & x \in A] by rewrite !inE (valP k). by exists [` kA]; rewrite // ?ffunE !getfE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)