proposition: Lemma catf_setr f g k (v : V) : f + g.[k <- v] = (f + g).[k <- v].
proof: Proof. apply/fmapP=> k'; rewrite !(fnd_cat, fnd_set, mem_setf, inE). by have [->|Nkk'] := altP eqP; do !case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)