Remove selector properties in group 1

CHANGELOG.md

@@ -2626,11 +2626,6 @@ Other minor changes
  lookup-cast₂ : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
  cast-reverse : cast eq ∘ reverse ≗ reverse ∘ cast eq
 
- head-singleton : head ≗ last {n = zero}
- head-init : head ∘ init ≗ head
- last-tail : last ∘ tail ≗ last
- init-tail : init ∘ tail ≗ tail ∘ init
-
  ++-assoc : cast eq ((xs ++ ys) ++ zs) ≡ xs ++ (ys ++ zs)
  ++-identityʳ : cast eq (xs ++ []) ≡ xs
  init-reverse : init ∘ reverse ≗ reverse ∘ tail

src/Data/Vec/Properties.agda

@@ -67,21 +67,6 @@ private
 
 -- See also Data.Vec.Properties.WithK.[]=-irrelevant.
 
-------------------------------------------------------------------------
--- selectors: head, tail, init and last
-
-head-singleton : head ≗ last {A = A} {n = zero}
-head-singleton (x ∷ []) = refl
-
-head-init : head ∘ init ≗ head {A = A} {n = suc n}
-head-init (x ∷ xs) = refl
-
-last-tail : last ∘ tail ≗ last {A = A} {n = suc n}
-last-tail (x ∷ xs) = refl
-
-init-tail : init ∘ tail ≗ tail ∘ init {A = A} {n = suc n}
-init-tail (x ∷ xs) = refl
-
 ------------------------------------------------------------------------
 -- take