proposition: Lemma domf_rem f A : domf f.[\ A] = domf f `\` A.
proof: Proof. by rewrite domf_restrict fsetIDAC fsetIid. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)