proposition: Lemma restrictf_mkdom f A : f.[& A] = f.[& domf f `&` A].
proof: Proof. apply/fmapP=> k; rewrite !fnd_restrict inE. by case: fndP => ?; rewrite ?(andbT, andbF) //=; case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)