proposition: Lemma setf_inj f f' k v : k \notin f -> k \notin f' -> f.[k <- v] = f'.[k <- v]-> f = f'.
proof: Proof. move=> kf kf' eq_fkv; apply/fmapP => k'. have := congr1 (fun g => g.[? k']) eq_fkv. by rewrite !fnd_set; case: eqP => // ->; rewrite !not_fnd. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)