proposition: Lemma domf_restrict f A : domf f.[& A] = A `&` domf f.
proof: Proof. by apply/fsetP=> k'; rewrite mem_restrictf !inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)