proposition: Lemma in_codomf_rem1 f (k : K) (kf : k \in domf f) : codomf f.[~ k] = if [exists k' : domf f, (val k' != k) && (f k' == f.[kf])] then codomf f else codomf f `\ f.[kf].
proof: Proof. apply/fsetP => v; rewrite codomf_rem_exists (fun_if (fun x => v \in x)) !(in_fset, inE). have [vf|vNf] := boolP (_ \in codomf f); rewrite /= ?(andbF,andbT) ?if_same //. rewrite -/(_ || _); apply/existsP/idP => /= [[k' /andP[xk /eqP <-]]|]. rewrite orbC -implybE; apply/implyP => eq_fk. by rewrite inE /= in xk; apply/existsP; exists k'; rewrite // xk eq_fk. have /imfsetP /= [[l lf] _ ->] := vf; rewrite orbC. have [->|neq_f _] := altP (f.[lf] =P _). by move=> /existsP [m /andP[Nmk /eqP <-]]; exists m; rewrite eqxx inE Nmk. exists [` lf]; rewrite eqxx andbT inE /=. apply: contra neq_f => /eqP eq_lk; rewrite eq_lk in lf *. by apply/eqP; congr f.[_]; apply: bool_irrelevance. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)