-- Return the biggest Fin we can
bound : Fin (S n);
bound {n=O} = fO;
bound {n=S k} = fS bound;

-- Generic environments, with R giving the type and iR giving the 
-- interpretation of the type.

using (R:#, r:R, ty:R, iR:R->#, xs:Vect R n) {

  data Env : (R:#) -> (iR:R->#) -> (xs:Vect R n) -> # where
     Empty : (Env R iR VNil)
   | Extend : (res:(iR r)) -> (Env R iR xs) -> 
	      (Env R iR (VCons r xs));

  envLookup : (i:Fin n) -> (Env R iR xs) -> (iR (vlookup i xs));
  envLookup fO (Extend t env) = t;
  envLookup (fS i) (Extend t env) = envLookup i env;

  update : (i:Fin n) -> A -> (Vect A n) -> (Vect A n);
  update fO v (VCons x xs) = VCons v xs;
  update (fS i) v (VCons x xs) = VCons x (update i v xs);

  updateEnv : {newR:R} -> (Env R iR xs) ->
	      (i:Fin n) -> (iR newR) ->
	      (Env R iR (update i newR xs));
  updateEnv (Extend t env) fO val = Extend val env;
  updateEnv (Extend t env) (fS i) val = Extend t (updateEnv env i val);

  snoc : (Vect A n) -> A -> (Vect A (S n));
  snoc VNil a = VCons a VNil;
  snoc (VCons x xs) a = VCons x (snoc xs a);

  -- Explicit rewrites are sometimes handy...
  snocCons : (x,v:A) -> (xs:Vect A n) -> ((VCons x (snoc xs v)) = (snoc (VCons x xs) v));
  snocCons x v xs = refl _;

  addEnd : (Env R iR xs) -> (r:iR ty) -> (Env R iR (snoc xs ty));
  addEnd Empty i = Extend i Empty;
  addEnd (Extend t env) i = Extend t (addEnd env i);

  dropEnd : (Env R iR (snoc xs x)) -> (Env R iR xs);
  dropEnd {xs=VNil} env = Empty;
  dropEnd {xs=VCons x xs} (Extend v env) = Extend v (dropEnd env);

}

weaken : (Fin n) -> (Fin (S n));
weaken fO = fO;
weaken (fS k) = fS (weaken k);

nweaken : {k:Nat} -> (Fin n) -> (Fin (plus k n));
nweaken {k=O} x = x;
nweaken {k=S n} x = weaken (nweaken x);