proposition: Lemma bseq0 : all_equal_to ([bseq] : 0.-bseq T).
proof: Proof. by move=> s; apply: val_inj; case: s => [[]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype path)