proposition: Lemma perm_flatten (ss1 ss2 : seq (seq T)) : perm_eq ss1 ss2 -> perm_eq (flatten ss1) (flatten ss2).
proof: Proof. move=> eq_ss; apply/permP=> a; apply/catCA_perm_subst: ss1 ss2 eq_ss. by move=> ss1 ss2 ss3; rewrite !flatten_cat !count_cat addnCA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)