Provide a proof of the vec_to_list correspondence.
We know by injectivity of vec_to_list_inj1 that two vectors of the same list have the same length, besides they are the same by inj2. So .... :
Theorem to_list_holds : forall a n (x : vec a n) (P : forall n, vector a n -> Prop), -> P _ (list_to_vec (vec_to_List l)) -> P _ x.