diff --git a/library/data/vector.lean b/library/data/vector.lean
index e7889d2c23..733ce54bf6 100644
--- a/library/data/vector.lean
+++ b/library/data/vector.lean
@@ -5,192 +5,147 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Module: data.vector
 Author: Floris van Doorn, Leonardo de Moura
 -/
+import data.nat.basic
+open nat prod
 
-import data.nat.basic data.empty data.prod
-open nat eq.ops prod
-
-inductive vector (T : Type) : ℕ → Type :=
-  nil {} : vector T 0,
-  cons : T → ∀{n}, vector T n → vector T (succ n)
+inductive vector (A : Type) : nat → Type :=
+  nil {} : vector A zero,
+  cons   : Π {n}, A → vector A n → vector A (succ n)
 
 namespace vector
   notation a :: b := cons a b
   notation `[` l:(foldr `,` (h t, cons h t) nil) `]` := l
 
   variables {A B C : Type}
-  variables {n m : nat}
 
-  protected definition is_inhabited [instance] (H : inhabited A) (n : nat) : inhabited (vector A n) :=
-  nat.rec_on n
-    (inhabited.mk nil)
-    (λ (n : nat) (iH : inhabited (vector A n)),
-      inhabited.destruct H
-        (λa, inhabited.destruct iH
-          (λv, inhabited.mk (a :: v))))
+  protected definition is_inhabited [instance] (h : inhabited A) : ∀ (n : nat), inhabited (vector A n),
+  is_inhabited 0     := inhabited.mk nil,
+  is_inhabited (n+1) := inhabited.mk (inhabited.value h :: inhabited.value (is_inhabited n))
 
-  theorem z_cases_on {C : vector A 0 → Type} (v : vector A 0) (Hnil : C nil) : C v :=
-  begin
-    cases v,
-    apply Hnil
-  end
+  theorem vector0_eq_nil : ∀ (v : vector A 0), v = nil,
+  vector0_eq_nil nil := rfl
 
-  theorem vector0_eq_nil (v : vector A 0) : v = nil :=
-  z_cases_on v rfl
+  definition head : Π {n : nat}, vector A (succ n) → A,
+  head (a::v) := a
 
-  protected definition destruct (v : vector A (succ n)) {P : Π {n : nat}, vector A (succ n) → Type}
-                      (H : Π {n : nat} (h : A) (t : vector A n), P (h :: t)) : P v :=
-  begin
-    cases v with (h', n', t'),
-    apply (H h' t')
-  end
+  definition tail : Π {n : nat}, vector A (succ n) → vector A n,
+  tail (a::v) := v
 
-  definition nz_cases_on := @destruct
-
-  definition head (v : vector A (succ n)) : A :=
-  destruct v (λ n h t, h)
-
-  definition tail (v : vector A (succ n)) : vector A n :=
-  destruct v (λ n h t, t)
-
-  theorem head_cons (h : A) (t : vector A n) : head (h :: t) = h :=
+  theorem head_cons {n : nat} (h : A) (t : vector A n) : head (h :: t) = h :=
   rfl
 
-  theorem tail_cons (h : A) (t : vector A n) : tail (h :: t) = t :=
+  theorem tail_cons {n : nat} (h : A) (t : vector A n) : tail (h :: t) = t :=
   rfl
 
-  theorem eta (v : vector A (succ n)) : head v :: tail v = v :=
-  destruct v (λ n h t, rfl)
+  theorem eta : ∀ {n : nat} (v : vector A (succ n)), head v :: tail v = v,
+  eta (a::v) := rfl
 
-  definition last : vector A (succ n) → A :=
-  nat.rec_on n
-    (λ (v : vector A (succ zero)), head v)
-    (λ n₁ r v, r (tail v))
+  definition last : Π {n : nat}, vector A (succ n) → A,
+  last (a::nil) := a,
+  last (a::v)   := last v
 
   theorem last_singleton (a : A) : last (a :: nil) = a :=
   rfl
 
-  theorem last_cons (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
+  theorem last_cons {n : nat} (a : A) (v : vector A (succ n)) : last (a :: v) = last v :=
   rfl
 
-  definition const (n : nat) (a : A) : vector A n :=
-  nat.rec_on n
-    nil
-    (λ n₁ r, a :: r)
+  definition const : Π (n : nat), A → vector A n,
+  const 0        a := nil,
+  const (succ n) a := a :: const n a
 
   theorem head_const (n : nat) (a : A) : head (const (succ n) a) = a :=
   rfl
 
-  theorem last_const (n : nat) (a : A) : last (const (succ n) a) = a :=
-  nat.induction_on n
-    rfl
-    (λ n₁ ih, ih)
+  theorem last_const : ∀ (n : nat) (a : A), last (const (succ n) a) = a,
+  last_const 0        a := rfl,
+  last_const (succ n) a := last_const n a
 
-  definition map (f : A → B) (v : vector A n) : vector B n :=
-  nat.rec_on n
-    (λ v, nil)
-    (λ n₁ r v, f (head v) :: r (tail v))
-    v
+  definition map (f : A → B) : Π {n : nat}, vector A n → vector B n,
+  map nil    := nil,
+  map (a::v) := f a :: map v
 
-  theorem map_vnil (f : A → B) : map f nil = nil :=
+  theorem map_nil (f : A → B) : map f nil = nil :=
   rfl
 
-  theorem map_vcons (f : A → B) (h : A) (t : vector A n) : map f (h :: t) =  f h :: map f t :=
+  theorem map_cons {n : nat} (f : A → B) (h : A) (t : vector A n) : map f (h :: t) =  f h :: map f t :=
   rfl
 
-  definition map2 (f : A → B → C) (v₁ : vector A n) (v₂ : vector B n) : vector C n :=
-  nat.rec_on n
-    (λ v₁ v₂, nil)
-    (λ n₁ r v₁ v₂, f (head v₁) (head v₂) :: r (tail v₁) (tail v₂))
-    v₁ v₂
+  definition map2 (f : A → B → C) : Π {n : nat}, vector A n → vector B n → vector C n,
+  map2 nil     nil     := nil,
+  map2 (a::va) (b::vb) := f a b :: map2 va vb
 
-  theorem map2_vnil (f : A → B → C) : map2 f nil nil = nil :=
+  theorem map2_nil (f : A → B → C) : map2 f nil nil = nil :=
   rfl
 
-  theorem map2_vcons (f : A → B → C) (h₁ : A) (h₂ : B) (t₁ : vector A n) (t₂ : vector B n) :
-                     map2 f (h₁ :: t₁) (h₂ :: t₂) = f h₁ h₂ :: map2 f t₁ t₂ :=
+  theorem map2_cons {n : nat} (f : A → B → C) (h₁ : A) (h₂ : B) (t₁ : vector A n) (t₂ : vector B n) :
+                    map2 f (h₁ :: t₁) (h₂ :: t₂) = f h₁ h₂ :: map2 f t₁ t₂ :=
   rfl
 
-  definition append (w : vector A n) (v : vector A m) : vector A (n ⊕ m) :=
-  rec_on w
-    v
-    (λ (a₁ : A) (n₁ : nat) (v₁ : vector A n₁) (r₁ : vector A (n₁ ⊕ m)), a₁ :: r₁)
+  -- Remark: why do we need to provide indices?
+  definition append : Π {n m : nat}, vector A n → vector A m → vector A (n ⊕ m),
+  @append 0        m nil    w := w,
+  @append (succ n) m (a::v) w := a :: (append v w)
 
-  theorem append_nil (v : vector A n) : append nil v = v :=
+  theorem append_nil {n : nat} (v : vector A n) : append nil v = v :=
   rfl
 
-  theorem append_cons (h : A) (t : vector A n) (v : vector A m) :
-    append (h :: t) v = h :: (append t v) :=
+  theorem append_cons {n m : nat} (h : A) (t : vector A n) (v : vector A m) :
+    append (h::t) v = h :: (append t v) :=
   rfl
 
-  definition unzip : vector (A × B) n → vector A n × vector B n :=
-  nat.rec_on n
-    (λ v, (nil, nil))
-    (λ a r v,
-      let t := r (tail v) in
-      (pr₁ (head v) :: pr₁ t, pr₂ (head v) :: pr₂ t))
+  definition unzip : Π {n : nat}, vector (A × B) n → vector A n × vector B n,
+  unzip nil           := (nil, nil),
+  unzip ((a, b) :: v) := (a :: pr₁ (unzip v), b :: pr₂ (unzip v))
 
-  definition zip : vector A n → vector B n → vector (A × B) n :=
-  nat.rec_on n
-    (λ v₁ v₂, nil)
-    (λ a r v₁ v₂, (head v₁, head v₂) :: r (tail v₁) (tail v₂))
-
-  theorem unzip_zip : ∀ (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂) :=
-  nat.induction_on n
-    (λ (v₁ : vector A zero) (v₂ : vector B zero),
-       z_cases_on v₁ (z_cases_on v₂ rfl))
-    (λ (n₁ : nat) (ih : ∀ (v₁ : vector A n₁) (v₂ : vector B n₁), unzip (zip v₁ v₂) = (v₁, v₂))
-       (v₁ : vector A (succ n₁)) (v₂ : vector B (succ n₁)), calc
-       unzip (zip v₁ v₂) = unzip ((head v₁, head v₂) :: zip (tail v₁) (tail v₂)) : rfl
-                     ... = (head v₁ :: pr₁ (unzip (zip (tail v₁) (tail v₂))),
-                            head v₂ :: pr₂ (unzip (zip (tail v₁) (tail v₂))))    : rfl
-                     ... = (head v₁ :: pr₁ (tail v₁, tail v₂),
-                            head v₂ :: pr₂ (tail v₁, tail v₂))                   : ih
-                     ... = (head v₁ :: tail v₁, head v₂ :: tail v₂)              : rfl
-                     ... = (v₁, head v₂ :: tail v₂)                              : vector.eta
-                     ... = (v₁, v₂)                                              : vector.eta)
-
-  theorem zip_unzip : ∀ (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v :=
-  nat.induction_on n
-    (λ (v : vector (A × B) zero),
-       z_cases_on v rfl)
-    (λ (n₁ : nat) (ih : ∀ v, zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v) (v : vector (A × B) (succ n₁)), calc
-       zip (pr₁ (unzip v)) (pr₂ (unzip v)) = zip (pr₁ (head v) :: pr₁ (unzip (tail v)))
-                                                 (pr₂ (head v) :: pr₂ (unzip (tail v)))                  : rfl
-                 ... = (pr₁ (head v), pr₂ (head v)) :: zip (pr₁ (unzip (tail v))) (pr₂ (unzip (tail v))) : rfl
-                 ... = (pr₁ (head v), pr₂ (head v)) :: tail v                                            : ih
-                 ... = head v :: tail v                                                                  : prod.eta
-                 ... = v                                                                                 : vector.eta)
-
-  /- Length -/
-
-  definition length (v : vector A n) :=
-  n
-
-  theorem length_nil : length (@nil A) = 0 :=
+  theorem unzip_nil : unzip (@nil (A × B)) = (nil, nil) :=
   rfl
 
-  theorem length_cons (a : A) (v : vector A n) : length (a :: v) = succ (length v) :=
+  theorem unzip_cons {n : nat} (a : A) (b : B) (v : vector (A × B) n) :
+       unzip ((a, b) :: v) = (a :: pr₁ (unzip v), b :: pr₂ (unzip v)) :=
   rfl
 
-  theorem length_append (v₁ : vector A n) (v₂ : vector A m) : length (append v₁ v₂) = length v₁ + length v₂ :=
-  calc length (append v₁ v₂) = length v₁ ⊕ length v₂ : rfl
-                         ... = length v₁ + length v₂ : add_eq_addl
+  definition zip : Π {n : nat}, vector A n → vector B n → vector (A × B) n,
+  zip nil     nil     := nil,
+  zip (a::va) (b::vb) := ((a, b) :: zip va vb)
+
+  theorem zip_nil_nil : zip (@nil A) (@nil B) = nil :=
+  rfl
+
+  theorem zip_cons_cons {n : nat} (a : A) (b : B) (va : vector A n) (vb : vector B n) :
+      zip (a::va) (b::vb) = ((a, b) :: zip va vb) :=
+  rfl
+
+  theorem unzip_zip : ∀ {n : nat} (v₁ : vector A n) (v₂ : vector B n), unzip (zip v₁ v₂) = (v₁, v₂),
+  @unzip_zip 0        nil     nil     := rfl,
+  @unzip_zip (succ n) (a::va) (b::vb) := calc
+       unzip (zip (a :: va) (b :: vb))
+             = (a :: pr₁ (unzip (zip va vb)), b :: pr₂ (unzip (zip va vb))) : rfl
+        ...  = (a :: pr₁ (va, vb), b :: pr₂ (va, vb))                       : {unzip_zip va vb}
+        ...  = (a :: va, b :: vb)                                           : rfl
+
+  theorem zip_unzip : ∀ {n : nat} (v : vector (A × B) n), zip (pr₁ (unzip v)) (pr₂ (unzip v)) = v,
+  @zip_unzip 0        nil            := rfl,
+  @zip_unzip (succ n) ((a, b) :: v)  := calc
+    zip (pr₁ (unzip ((a, b) :: v))) (pr₂ (unzip ((a, b) :: v)))
+         = (a, b) :: zip (pr₁ (unzip v)) (pr₂ (unzip v)) : rfl
+     ... = (a, b) :: v                                   : {zip_unzip v}
 
   /- Concat -/
 
-  definition concat (v : vector A n) (a : A) : vector A (succ n) :=
-  vector.rec_on v
-    (a :: nil)
-    (λ h n t r, h :: r)
+  definition concat : Π {n : nat}, vector A n → A → vector A (succ n),
+  concat nil    a := a :: nil,
+  concat (b::v) a := b :: concat v a
 
   theorem concat_nil (a : A) : concat nil a = a :: nil :=
   rfl
 
-  theorem last_concat (v : vector A n) (a : A) : last (concat v a) = a :=
-  vector.induction_on v
-    rfl
-    (λ h n t ih, calc
-      last (concat (h :: t) a) = last (concat t a) : rfl
-                           ... = a                 : ih)
+  theorem concat_cons {n : nat} (b : A) (v : vector A n) (a : A) : concat (b :: v) a = b :: concat v a :=
+  rfl
 
+  theorem last_concat : ∀ {n : nat} (v : vector A n) (a : A), last (concat v a) = a,
+  @last_concat 0        nil    a := rfl,
+  @last_concat (succ n) (b::v) a := calc
+    last (concat (b::v) a) = last (concat v a) : rfl
+                    ...    = a                 : last_concat v a
 end vector