proposition: Lemma catCons {n1 n2 A} (a:A) (aa:n1.-tuple A) (bb:n2.-tuple A) : cat_tuple [tuple of a::aa] bb = [tuple of a::cat_tuple aa bb].
proof: Proof. by apply: eq_from_tnth=> i; rewrite !(tnth_nth a). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrnat eqtype seq fintype tuple)