proposition: Lemma restrictf_set f A (k : K) (v : V) : f.[k <- v].[& A] = if k \in A then f.[& A].[k <- v] else f.[& A].
proof: Proof. apply/fmapP => k' /=; rewrite !(fnd_if, fnd_set, fnd_restrict). by case: eqP => [->|]; do !case: ifP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)