proposition: Lemma injective_sigma : injective sigma.
proof: Proof. move=> i j; rewrite /sigma => /eqP ij; apply/eqP; move: ij. apply: contraTT => ij. apply/negP => /eqP. move/(congr1 (@nat_of_ary t')). rewrite !nat_of_ary_cat !(nat_of_ary_nseq0,mul0n,add0n). by rewrite !ary_of_natK => /injective_w/eqP; apply/negP. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext