proposition: Lemma codomf_restrict_exists f (A : {fset K}) : codomf f.[& A] = [fset v in codomf f | [exists k : domf f, (val k \in A) && (f k == v)]].
proof: Proof. rewrite codomf_restrict; apply/fsetP => v; rewrite !(in_fset, inE) /=; apply/imfsetP/idP. by move=> [k kA ->]; rewrite in_codomf /=; apply/existsP; exists k; apply/andP. by move=> /andP[fkdom /existsP [k /andP[kA /eqP<-]]]; exists k. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)