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