proposition: Lemma setfNK V (f : {fmap K -> V}) (k k' : K) (v : V) (k'f : k' \in _) (k'f' : k' \in _): f.[k <- v].[k'f'] = if k' == k then v else f.[k'f].
proof: Proof. by apply: Some_inj; rewrite Some_fnd !fnd_set in_fnd; case: ifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)