fact: Fixpoint vector_to_list (n:nat)(v:t A n){struct v} : list A := match v with | nil _ => List.nil | cons _ a p tl => List.cons a (vector_to_list p tl) end.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector