Load "basics.tt";
Load "fin.tt";

Data Vect (A:*):(n:Nat)* 
    = vnil:Vect A O
    | vcons:(k:Nat)(x:A)(xs:Vect A k)Vect A (S k);

Match lookup : (A:*)(n:Nat)(i:Fin n)(xs:Vect A n)A =
    lookup _ _ (fz _) (vcons _ _ x xs) = x
  | lookup _ _ (fs _ i) (vcons _ _ x xs) = lookup _ _ i xs;

testvect = vcons _ _ O (vcons _ _ (S O) (vcons _ _ (S (S O)) (vnil Nat)));
testfin = fs _ (fz (S O));