Section Zip.

Inductive Vec (A : Set) : nat -> Set :=
| vnil : Vec A 0
| vcons : forall n, A -> Vec A n -> Vec A (S n).

Definition v1 := vcons _ _ 2 (vcons _ _ 3 (vnil _)).
Definition v2 := vcons _ _ true (vcons _ _ false (vnil _)).

(* Implement zipping of vectors, either as term or via the interactive 
proof interface.

Fixpoint zip (A B : Set) (n : nat) (v1 : Vec A n) (v2 : Vec B n)
  : Vec (A * B) n.

Definition zip (A B : Set) (n : nat) (v1 : Vec A n) (v2 : Vec B n)
  : Vec (A * B) n.

*)