Thanks to Adam Chlipala for teaching me how to prove vec2list2vec. It means that converting a dependently typed vector to an ordinary list and back yields the same vector intact. But surely there is a simpler way?

Require Import List.

Require String.
Open Scope string_scope.
Ltac move_to_top x :=
  match reverse goal with
  | H : _ |- _ => try move x after H
  end.
Tactic Notation "assert_eq" ident(x) constr(v) :=
  let H := fresh in
  assert (x = v) as H by reflexivity;
  clear H.
Tactic Notation "Case_aux" ident(x) constr(name) :=
  first [
    set (x := name); move_to_top x
  | assert_eq x name; move_to_top x
  | fail 1 "because we are working on a different case" ].
Ltac Case name := Case_aux Case name.
Ltac SCase name := Case_aux SCase name.

Inductive vec (X: Type): nat -> Type :=
  | vnil: vec X 0
  | vcons: forall n: nat, X -> vec X n -> vec X (S n).

Implicit Arguments vnil [ [X] ].
Implicit Arguments vcons [ [X] [n] ].

Check (vcons 4 (vcons 2 (vcons 7 vnil))).

Fixpoint vec2list {X: Type} {n: nat} (v: vec X n): list X :=
  match v with
  | vnil => nil
  | vcons _ h t => cons h (vec2list t)
  end.

Fixpoint list2vec {X: Type} (l: list X): vec X (length l) :=
  match l with
  | nil => vnil
  | cons h t => vcons h (list2vec t)
  end.

Theorem vec2list_length: forall (X: Type) (n: nat) (v: vec X n),
  length (vec2list v) = n.
Proof.
  intros X n v. induction v as [| n' h t].
  Case "vnil". reflexivity.
  Case "vcons". simpl. rewrite -> IHt. reflexivity.
Qed.

Theorem list2vec2list: forall (X: Type) (l: list X),
  vec2list (list2vec l) = l.
Proof.
  intros X l. induction l as [| h t].
  Case "nil". reflexivity.
  Case "cons". simpl. rewrite -> IHt. reflexivity.
Qed.

Require Import Eqdep.
Lemma vec2list2vec': forall (X: Type) (l: list X) (n: nat) (v: vec X n),
  forall (EQ: length l = n), l = vec2list v ->
    v = match EQ in (_ = n) return vec _ n with
          | refl_equal => list2vec l
        end.
Proof.
  intros X l.
  induction l as [| h t]; simpl;
    intros n v EQ H; destruct v; inversion EQ as [EQ'].
  Case "nil". rewrite (UIP_refl _ _ EQ). reflexivity.
  Case "cons". inversion H. rewrite (IHt _ v EQ' H2). clear.
    generalize (list2vec t) EQ EQ'.
    rewrite EQ'. intros v EQ1 EQ2.
    rewrite (UIP_refl _ _ EQ1).
    rewrite (UIP_refl _ _ EQ2).
    reflexivity.
Qed.

Theorem vec2list2vec: forall (X: Type) (n: nat) (v: vec X n),
  v = match (vec2list_length X n v) in (_ = n) return vec _ n with
        | refl_equal => list2vec (vec2list v)
      end.
Proof.
  intros. apply vec2list2vec'. reflexivity.
Qed.