proposition: Lemma bseq_tagged_tuple_bij {n T} : bijective (@bseq_tagged_tuple n T).
proof: Proof. exact/Bijective/tagged_tuple_bseqK/bseq_tagged_tupleK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)