@@ -447,6 +447,18 @@ range : Vect n (Fin n)
447range {n=Z} = []
447range {n=Z} = []
448range {n=S _} = fZ :: map fS range
448range {n=S _} = fZ :: map fS range
451+--------------------------------------------------------------------------------
453+--------------------------------------------------------------------------------
455+vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
456+vectNilRightNeutral [] = refl
457+vectNilRightNeutral (x :: xs) = tailCong _ _ (vectNilRightNeutral xs)
458+ where tailCong : (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)
459+ tailCong xs xs refl = refl
450--------------------------------------------------------------------------------
462--------------------------------------------------------------------------------
452--------------------------------------------------------------------------------
464--------------------------------------------------------------------------------