proposition: Lemma catf_setl f g k (v : V) : f.[k <- v] + g = if k \in g then f + g else (f + g).[k <- v].
proof: Proof. apply/fmapP=> k'; rewrite !(fnd_if, fnd_cat, fnd_set). 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)