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