@@ -447,6 +447,18 @@ range : Vect n (Fin n)
447447range {n=Z} = []
448448range {n=S _} = fZ :: map fS range
449449
450+
451+--------------------------------------------------------------------------------
452+-- Properties
453+--------------------------------------------------------------------------------
454+
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
460+
461+
450462--------------------------------------------------------------------------------
451463-- Proofs
452464--------------------------------------------------------------------------------