proposition: Lemma widen_bseq_in_bseq n (bs : n.-bseq T) : widen_bseq (size_bseq bs) (in_bseq bs) = bs.
proof: Proof. exact: val_inj. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)