proposition: Theorem decomp : forall (A : Set) (n : nat) (v : Vector.t A (S n)), v = Vector.cons (Vector.hd v) (Vector.tl v).
proof: Proof. intros. change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _ (S n) v). apply Vid_eq. Defined.
imports: Arith Vector List Extraction ZArith Compare_dec ZArith List Wf_nat