proposition: Lemma catfA f g h : f + (g + h) = f + g + h.
proof: Proof. by apply/fmapP => k; rewrite !fnd_cat !mem_catf; do !case: (_ \in _). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)