proposition: Theorem vector_eta : forall n (v : vector T n), v = match n as n return vector T n -> vector T n with | 0 => fun _ => Vnil _ | S n => fun v => Vcons (vector_hd v) (vector_tl v) end v.
proof: Proof. destruct v; auto. Qed.
imports: ExtLib.Data.Fin