proposition: Lemma codomf_rem_exists f (A : {fset K}) : codomf f.[\ A] = [fset v in codomf f | [exists k : domf f, (val k \notin A) && (f k == v)]].
proof: Proof. rewrite codomf_restrict_exists; apply: eq_imfset => x //=. rewrite !inE; case: (_ \in _) => //=. apply/existsP/existsP => [] /= [k]; rewrite ?inE; by do 2?[move=>/andP []]; exists k; rewrite ?inE; do 2?[apply/andP; split]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)