proposition: Lemma shape_map_tab (t : seq (seq T1)) : shape [seq map F r | r <- t] = shape t.
proof: Proof. by rewrite /shape -map_comp; apply eq_map => s /=; rewrite size_map. Qed.
imports: HB(structures) mathcomp(all_ssreflect) tools partition ordtype sorted