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