A list transformed from a vector equals to a list transformed from a vector casted its type

Question

I want to prove equality on list.

Require Import Coq.Vectors.Vector.
Require Import CoLoR.Util.Vector.VecUtil.

Lemma Vcast_eq : forall (A:Type)(n m:nat)(v:t A n)(p:n=m),
      to_list v = to_list (Vcast v p).
Proof.
induction v.
destruct (Vcast Vnil p); trivial.
inversion p.
Abort.

I'm sure that its two lists are equal because I only casted type of original vector.

Please tell me how to prove any more.

Answer 1

I have proved on my own.

Require Import Coq.Vectors.Vector.
Require Import CoLoR.Util.Vector.VecUtil.
Require Import Coq.Lists.List.

Lemma to_list_cons (A:Type)(n:nat)(a:A)(v:t A n): to_list (Vcons a v) = a :: (to_list v).
Proof.
reflexivity.
Qed.

Lemma Vcast_eq (A:Type): forall (n:nat)(v:t A n)(m:nat)(p:n=m),
      to_list v = to_list (Vcast v p).
Proof.
induction v.
intros; destruct (Vcast Vnil p); trivial.
inversion p.
intros.
destruct m.
inversion p.
rewrite Vcast_cons.
remember (eq_add_S p).
rewrite !to_list_cons.
f_equal.
apply (IHv m e).
Qed.