associativity for vectors

CHANGELOG.md

@@ -716,6 +716,15 @@ Other minor changes
          → dsubst₂ C p q (f x₁ y₁) ≡ f x₂ y₂
   ```
 
+* Added vector associativity proof to 
+  `Data/Vec/Relation/Binary/Equality/Setoid.agda`:
+  ```
+  ++-assoc : ∀ {n m k} (xs : Vec A n) → (ys : Vec A m) 
+      → (zs : Vec A k) → (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs)
+  ++-assoc [] ys zs = ≋-refl
+  ++-assoc (x ∷ xs) ys zs = refl ∷ ++-assoc xs ys zs
+  ```
+
 NonZero/Positive/Negative changes
 ---------------------------------
 

src/Data/Vec/Relation/Binary/Equality/Setoid.agda

@@ -68,6 +68,11 @@ open PW public using (++⁺ ; ++⁻ ; ++ˡ⁻; ++ʳ⁻)
 ++-identityʳ []       = []
 ++-identityʳ (x ∷ xs) = refl ∷ ++-identityʳ xs
 
+++-assoc : ∀ {n m k} (xs : Vec A n) (ys : Vec A m) (zs : Vec A k) → 
+             (xs ++ ys) ++ zs ≋ xs ++ (ys ++ zs)
+++-assoc [] ys zs = ≋-refl
+++-assoc (x ∷ xs) ys zs = refl ∷ ++-assoc xs ys zs
+
 map-++-commute : ∀ {b m n} {B : Set b}
                    (f : B → A) (xs : Vec B m) {ys : Vec B n} →
                    map f (xs ++ ys) ≋ map f xs ++ map f ys