@@ -452,11 +452,18 @@ range {n=S _} = fZ :: map fS range
452-- Properties
452-- Properties
453--------------------------------------------------------------------------------
453--------------------------------------------------------------------------------
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
455vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
458vectNilRightNeutral : (xs : Vect n a) -> xs ++ [] = xs
456vectNilRightNeutral [] = refl
459vectNilRightNeutral [] = refl
457−vectNilRightNeutral (x :: xs) = tailCong _ _ (vectNilRightNeutral xs)
460+vectNilRightNeutral (x :: xs) =
458− where tailCong : (xs : Vect n a) -> (ys : Vect m a) -> (xs = ys) -> (x :: xs = x :: ys)
461+ vectConsCong _ _ _ (vectNilRightNeutral xs)
459− tailCong xs xs refl = refl
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)
462--------------------------------------------------------------------------------
469--------------------------------------------------------------------------------