proposition: Lemma setf_rem f A (k : K) (v : V) : f.[\ A].[k <- v] = f.[k <- v].[\ (A `\ k)].
proof: Proof. by rewrite setf_restrict fsetUDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)