proposition: Lemma eq_from_flatten_shape ss1 ss2 : flatten ss1 = flatten ss2 -> shape ss1 = shape ss2 -> ss1 = ss2.
proof: Proof. by move=> Eflat Esh; rewrite -[LHS]flattenK Eflat Esh flattenK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)