Match the order of ++-identityʳ with that of lists

Author: shhyou

CHANGELOG.md

@@ -2632,7 +2632,7 @@ Other minor changes
   init-tail      : init ∘ tail ≗ tail ∘ init
 
   ++-assoc     : cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
-  ++-identityʳ : cast eq xs ≡ xs ++ []
+  ++-identityʳ : cast eq (xs ++ []) ≡ xs
   init-reverse : init ∘ reverse ≗ reverse ∘ tail
   last-reverse : last ∘ reverse ≗ head
   reverse-++   : cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs

src/Data/Vec/Properties.agda

@@ -493,7 +493,7 @@ map-⊛ f g (x ∷ xs) = cong (f x (g x) ∷_) (map-⊛ f g xs)
 ++-assoc eq []       ys zs = cast-is-id eq (ys ++ zs)
 ++-assoc eq (x ∷ xs) ys zs = cong (x ∷_) (++-assoc (cong pred eq) xs ys zs)
 
-++-identityʳ : ∀ .(eq : m ≡ m + zero) (xs : Vec A m) → cast eq xs ≡ xs ++ []
+++-identityʳ : ∀ .(eq : n + zero ≡ n) (xs : Vec A n) → cast eq (xs ++ []) ≡ xs
 ++-identityʳ eq []       = refl
 ++-identityʳ eq (x ∷ xs) = cong (x ∷_) (++-identityʳ (cong pred eq) xs)
 
@@ -965,7 +965,12 @@ map-reverse f (x ∷ xs) = begin
 
 reverse-++ : ∀ .(eq : m + n ≡ n + m) (xs : Vec A m) (ys : Vec A n) →
              cast eq (reverse (xs ++ ys)) ≡ reverse ys ++ reverse xs
-reverse-++ {m = zero}  {n = n} eq []       ys = ++-identityʳ (+-comm zero n) (reverse ys)
+reverse-++ {m = zero}  {n = n} eq []       ys = begin
+  cast _ (reverse ys)                ≡˘⟨ cong (cast eq) (++-identityʳ (sym eq) (reverse ys)) ⟩
+  cast _ (cast _ (reverse ys ++ [])) ≡⟨ cast-trans (sym eq) eq (reverse ys ++ []) ⟩
+  cast _ (reverse ys ++ [])          ≡⟨ cast-is-id (trans (sym eq) eq) (reverse ys ++ []) ⟩
+  reverse ys ++ []                   ≡⟨⟩
+  reverse ys ++ reverse []           ∎
 reverse-++ {m = suc m} {n = n} eq (x ∷ xs) ys = begin
   cast eq (reverse (x ∷ xs ++ ys))                ≡⟨ cong (cast eq) (reverse-∷ x (xs ++ ys)) ⟩
   cast eq (reverse (xs ++ ys) ∷ʳ x)               ≡˘⟨ cast-trans eq₂ eq₁ (reverse (xs ++ ys) ∷ʳ x) ⟩