fact: Fixpoint list_to_vector (l:list A) : t A (length l) := match l as x return t A (length x) with | List.nil => nil A | List.cons a tl => cons A a (length tl)(list_to_vector tl) end.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector