proposition: Lemma restrictf_cat f g A : (f + g).[& A] = f.[& A] + g.[& A].
proof: Proof. apply/fmapP => k'; rewrite !(fnd_cat, fnd_restrict) mem_restrictf. by case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)