proposition: Lemma bseq_tagged_tupleK {n T} : cancel (@bseq_tagged_tuple n T) tagged_tuple_bseq.
proof: Proof. by move=> bs; apply/val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)