proposition: Lemma bigcat_free : directv (\sum_(i | P i) <<Xs i>>) -> (forall i, P i -> free (Xs i)) -> free (\big[cat/[::]]_(i | P i) Xs i).
proof: Proof. rewrite /free directvE /= span_bigcat => /directvP-> /= freeXs. rewrite (big_morph _ (@size_cat _) (erefl _)) /=. by apply/eqP/eq_bigr=> i /freeXs/eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)