@@ -452,11 +452,18 @@ range {n=S _} = fZ :: map fS range
452452-- Properties
453453--------------------------------------------------------------------------------
454454
455+vectConsCong : (x : a) -> (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)
456+vectConsCong x xs xs refl = refl
457+
455458vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
456459vectNilRightNeutral [] = 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+vectNilRightNeutral (x :: xs) =
461+ vectConsCong _ _ _ (vectNilRightNeutral xs)
462+
463+vectAppendAssociative : (x : Vect xLen a) -> (y : Vect yLen a) -> (z : Vect zLen a) -> x ++ (y ++ z) = (x ++ y) ++ z
464+vectAppendAssociative [] y z = refl
465+vectAppendAssociative (x :: xs) ys zs =
466+ vectConsCong _ _ _ (vectAppendAssociative xs ys zs)
460467
461468
462469--------------------------------------------------------------------------------