fact: Definition of_list_length (A : Set)(m : nat)(ls : list A)(pf : length ls = m) : Vector.t A m := match pf with | eq_refl => Vector.of_list ls end.
imports: FCF.StdNat List Bvector micromega.Lia FCF.EqDec FCF.Fold ZArith