proposition: Theorem vect_to_list_and_back : forall n (v:t A n), JMeq v (list_to_vector (vector_to_list n v)).
proof: Proof. intros n v; induction v as [ | h n v IHv]. - reflexivity. - simpl; apply Vconseq. + now rewrite keep_length. + assumption. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector