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