proposition: Lemma codomf_set f (k : K) (v : V) (kf : k \in domf f) : codomf f.[k <- v] = v |` codomf f.[~ k].
proof: Proof. rewrite -setf_rem1; apply/fsetP=> v'; rewrite !inE. have [->|neq_v'v] /= := altP eqP. by apply/codomfP; exists k; rewrite fnd_set eqxx. apply/codomfP/codomfP => [] [k' fk'_eq]; exists k'; move: fk'_eq; rewrite fnd_set. by have [_ [eq_vv']|//] := altP eqP; rewrite eq_vv' eqxx in neq_v'v *. by have [->|//] := altP eqP; rewrite fnd_rem inE eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)