diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4448791d5a..43031ac590 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1139,6 +1139,31 @@ Deprecated names
   map-++-commute ↦  map-++
   ```
 
+* In `Data.Vec.Relation.Unary.All`:
+  for `{{NonZero n}}`, as per issue #1686
+
+  ```agda
+  head′ : All P xs → P (Vec.head′ {n = n} xs)
+  tail′ : All P xs → All P (Vec.tail′ {n = n} xs)
+  uncons′ : All P xs → P (Vec.head′ {n = n} xs) × All P (Vec.tail′ {n = n} xs)
+  ```
+
+* In `Data.Vec.Relation.Unary.Any`:
+  for `{{NonZero n}}`, as per issue #1686
+
+  ```agda
+  head′ : ¬ Any P (Vec.tail′ {n = n} xs) → Any P xs → P (Vec.head′ {n = n} xs)
+  tail′ : ¬ P (Vec.head′ {n = n} xs) → Any P xs → Any P (Vec.tail′ {n = n} xs)
+  ```
+
+* In `Data.Vec.Relation.Unary.Linked.Properties`:
+  for `{{NonZero n}}`, as per issue #1686
+
+  ```agda
+  Linked⇒All′ : ∀ {v} {xs : Vec _ n} → R v (head′ xs) →
+                Linked R xs → All (R v) xs
+  ```
+
 * In `Function.Construct.Composition`:
   ```
   _∘-⟶_   ↦   _⟶-∘_
@@ -1557,6 +1582,8 @@ Other minor changes
   leftSemimedial : LeftSemimedial _∙_
   rightSemimedial : RightSemimedial _∙_
   middleSemimedial : ∀ x y z → (x ∙ y) ∙ (z ∙ x) ≈ (x ∙ z) ∙ (y ∙ x)
+
+  sum-remove′ : ∀ {n} {{_ : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (remove′ i t)
   ```
 
 * Added new proofs to `Algebra.Properties.Semigroup`:
@@ -1627,6 +1654,21 @@ Other minor changes
   quotient  : Fin (m * n) → Fin m
   remainder : Fin (m * n) → Fin n
   ```
+  
+  Additionally, as per issue #1686, primed functionality in cases
+  where the `Fin` index `n` is `NonZero`: 
+  ```
+  zero′     : Fin n
+  suc'      : Fin (ℕ.pred n) → Fin n
+  inject!′  : {i : Fin n} → Fin′ i → Fin (ℕ.pred n)
+  inject₁′  : Fin (ℕ.pred n) → Fin n
+  lower₁′   : (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n)
+  _ℕ-′_     : (j : Fin n) → Fin (n ℕ.∸ toℕ j)
+  _ℕ-ℕ′_    : Fin n → ℕ
+  punchOut′ : {i j : Fin n} → i ≢ j → Fin (ℕ.pred n)
+  punchIn′  : Fin n → Fin (ℕ.pred n) → Fin n
+  pinch′    : Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n)
+  ```	
 
 * Added new proofs in `Data.Fin.Induction`:
   every (strict) partial order is well-founded and Noetherian.
@@ -1691,6 +1733,29 @@ Other minor changes
   cast-trans    : cast eq₂ (cast eq₁ k) ≡ cast (trans eq₁ eq₂) k
   ```
 
+  Additionally properties of the primed functionality as in `Data.Fin.Base`:
+  ```
+  inject₁-lower₁′ : (n≢i+1 : n ≢ suc (toℕ i)) →
+                   inject₁′ (lower₁′ i n≢i+1) ≡ i
+  lower₁-irrelevant′ : (n≢i₁+1 n≢i₂+1 : n ≢ suc (toℕ i)) →
+                       lower₁′ i n≢i₁+1 ≡ lower₁′ i n≢i₂+1
+  inject₁≡⇒lower₁≡′ : (n≢j+1 : n ≢ suc (toℕ j)) → inject₁′ i ≡ j → lower₁′ j n≢j+1 ≡ i
+  pred<′ : (i : Fin n) → i ≢ zero′ → pred i < i
+  punchOut-cong′ : {i≢j : i ≢ j} {i≢k : i ≢ k} →
+                  j ≡ k → punchOut′ i≢j ≡ punchOut′ i≢k
+  punchOut-injective′ : (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                       punchOut′ i≢j ≡ punchOut′ i≢k → j ≡ k
+  punchIn-punchOut′ : {i j : Fin n} (i≢j : i ≢ j) →
+                     punchIn′ i (punchOut′ i≢j) ≡ j
+
+  pinch-injective′ : {i : Fin (ℕ.pred n)} {j k : Fin n} →
+                     suc′ i ≢ j → suc′ i ≢ k → pinch′ i j ≡ pinch′ i k → j ≡ k
+  ```
+
+  NB Adding `punchOut-cong′` for the sake of uniformity with the 'primed' naming scheme
+  for  `NonZero` instances, entailed renaming the old `punchOut-cong′` to `punchOut-cong-eq`,
+  with knock-on effect in two places in `Data.Fin.Permutation`
+
 * Added new functions in `Data.Integer.Base`:
   ```
   _^_ : ℤ → ℕ → ℤ
@@ -2044,12 +2109,33 @@ Other minor changes
 
   cast : .(eq : m ≡ n) → Vec A m → Vec A n
   ```
+  And for `{{NonZero n}}` as per issue 1686
+  ```
+  head′   : Vec A n → A
+  tail′   : Vec A n → A ^ (pred n)
+  uncons′ : Vec A n → A × Vec A (pred n)
+  insert′ : Vec A (pred n) → Fin n → A → Vec A n
+  remove′ : Vec A n → Fin n → Vec A (pred n)
+  init′   : (xs : Vec A n) → Vec A (pred n)
+  last′   : (xs : Vec A n) → A
+  ```
 
 * Added new instance in `Data.Vec.Categorical`:
   ```agda
   monad : RawMonad (λ (A : Set a) → Vec A n)
   ```
 
+* Added new functions in `Data.Vec.Functional` for `{{NonZero n}}`:
+  ```
+  head′   : Vector A n → A
+  tail′   : Vector A n → A ^ (pred n)
+  uncons′ : Vector A n → A × Vector A (pred n)
+  insert′ : Vector A (pred n) → Fin n → A → Vector A n
+  remove′ : Vector A n → Fin n → Vector A (pred n)
+  init′   : (xs : Vector A n) → Vector A (pred n)
+  last′   : (xs : Vector A n) → A
+  ```
+
 * Added new proofs in `Data.Vec.Properties`:
   ```agda
   padRight-refl      : padRight ≤-refl a xs ≡ xs
@@ -2111,6 +2197,20 @@ Other minor changes
   lookup-cast₁  : lookup (cast eq xs) i ≡ lookup xs (Fin.cast (sym eq) i)
   lookup-cast₂  : lookup xs (Fin.cast eq i) ≡ lookup (cast (sym eq) xs) i
   ```
+  And for `{{NonZero n}}`:
+  ```
+  insert-lookup′ : (xs : Vec A (pred n)) (i : Fin n) (v : A) →
+                  lookup (insert′ xs i v) i ≡ v
+  insert-punchIn′ : (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) →
+                   lookup (insert′ xs i v) (Fin.punchIn′ i j) ≡ lookup xs j
+
+  ```
+* Added new functions in `Data.Vec.Recursive` for `{{NonZero n}}`:
+  ```
+  uncons′ : A ^ n → A × A ^ (pred n)
+  head′   : A ^ n → A
+  tail′   : A ^ n → A ^ (pred n)
+  ```
 
 * Added new proofs in `Data.Vec.Functional.Properties`:
   ```
diff --git a/src/Algebra/Properties/CommutativeMonoid/Sum.agda b/src/Algebra/Properties/CommutativeMonoid/Sum.agda
index 54731cfb5b..c4bf6e45c0 100644
--- a/src/Algebra/Properties/CommutativeMonoid/Sum.agda
+++ b/src/Algebra/Properties/CommutativeMonoid/Sum.agda
@@ -59,6 +59,9 @@ sum-remove {suc n} {suc i}  xs = begin
   ∑t = sum t
   ∑t′ = sum (remove i t)
 
+sum-remove′ : ∀ {n} {{_ : NonZero n}} {i : Fin n} t → sum t ≈ t i + sum (remove′ i t)
+sum-remove′ {n = suc n} = sum-remove
+
 -- The '∑' operator distributes over addition.
 ∑-distrib-+ : ∀ {n} (f g : Vector Carrier n) → ∑[ i < n ] (f i + g i) ≈ ∑[ i < n ] f i + ∑[ i < n ] g i
 ∑-distrib-+ {zero}  f g = sym (+-identityˡ _)
diff --git a/src/Data/Fin/Base.agda b/src/Data/Fin/Base.agda
index 06c4581337..d5918912e6 100644
--- a/src/Data/Fin/Base.agda
+++ b/src/Data/Fin/Base.agda
@@ -7,13 +7,14 @@
 -- Note that elements of Fin n can be seen as natural numbers in the
 -- set {m | m < n}. The notation "m" in comments below refers to this
 -- natural number view.
+
 {-# OPTIONS --without-K --safe #-}
 
 module Data.Fin.Base where
 
 open import Data.Bool.Base using (Bool; true; false; T; not)
 open import Data.Empty using (⊥-elim)
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; z≤n; s≤s; z<s; s<s; _^_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; z≤n; s≤s; z<s; s<s; _^_)
 open import Data.Product as Product using (_×_; _,_; proj₁; proj₂)
 open import Data.Sum.Base as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
 open import Function.Base using (id; _∘_; _on_; flip)
@@ -38,6 +39,27 @@ data Fin : ℕ → Set where
   zero : Fin (suc n)
   suc  : (i : Fin n) → Fin (suc n)
 
+------------------------------------------------------------------------
+-- Much of the power of dependently-typed programming comes from the
+-- ability of pattern-matching over inhomogeneous telescopes of types
+-- to discriminate aruments to functions in sharper ways.
+
+-- The Fin type exemplifies this behaviour, but at the cost of not always
+-- being able to know in a function defintion which case one is in by virtue
+-- of an explicit constructor (ℕ.suc) symbol occurring in the type. So
+-- (issue #1686) we also consider constructors and functions defined over
+-- homogeneous telescopes of the form  {n} (i : Fin n) subject to n being
+-- NonZero, to be instantiated at any cal-site by instance inference.
+-- This additional functionality will be systematically marked by use of a prime \'.
+
+-- homogeneous constructors
+
+zero′ : .{{NonZero n}} → Fin n
+zero′ {n = suc _} = zero
+
+suc′ : .{{NonZero n}} → Fin (ℕ.pred n) → Fin n
+suc′ {n = suc _} = suc
+
 -- A conversion: toℕ "i" = i.
 
 toℕ : Fin n → ℕ
@@ -111,21 +133,31 @@ inject! : ∀ {i : Fin (suc n)} → Fin′ i → Fin n
 inject! {n = suc _} {i = suc _}  zero    = zero
 inject! {n = suc _} {i = suc _}  (suc j) = suc (inject! j)
 
+inject!′ : .{{NonZero n}} → {i : Fin n} → Fin′ i → Fin (ℕ.pred n)
+inject!′ {n = suc _} = inject!
+
 inject₁ : Fin n → Fin (suc n)
 inject₁ zero    = zero
 inject₁ (suc i) = suc (inject₁ i)
 
+inject₁′ : .{{NonZero n}} → Fin (ℕ.pred n) → Fin n
+inject₁′ {n = suc _} = inject₁
+
 inject≤ : Fin m → m ℕ.≤ n → Fin n
 inject≤ {_} {suc n} zero    _        = zero
 inject≤ {_} {suc n} (suc i) (s≤s m≤n) = suc (inject≤ i m≤n)
 
 -- lower₁ "i" _ = "i".
 
-lower₁ : ∀ (i : Fin (suc n)) → n ≢ toℕ i → Fin n
+lower₁ : (i : Fin (suc n)) → n ≢ toℕ i → Fin n
 lower₁ {zero}  zero    ne = ⊥-elim (ne refl)
 lower₁ {suc n} zero    _  = zero
 lower₁ {suc n} (suc i) ne = suc (lower₁ i (ne ∘ cong suc))
 
+lower₁′ : .{{NonZero n}} →
+          (i : Fin n) → n ≢ suc (toℕ i) → Fin (ℕ.pred n)
+lower₁′ {n = suc _} i ne = lower₁ i (ne ∘ cong suc)
+
 -- A strengthening injection into the minimal Fin fibre.
 strengthen : ∀ (i : Fin n) → Fin′ (suc i)
 strengthen zero    = zero
@@ -222,20 +254,26 @@ suc i - suc j  = i - j
 
 -- m ℕ- "i" = "m ∸ i".
 
-infixl 6 _ℕ-_
+infixl 6 _ℕ-_ _ℕ-′_
 
 _ℕ-_ : (n : ℕ) (j : Fin (suc n)) → Fin (suc n ℕ.∸ toℕ j)
 n     ℕ- zero   = fromℕ n
 suc n ℕ- suc i  = n ℕ- i
 
+_ℕ-′_ : (n : ℕ) {{_ : NonZero n}} (j : Fin n) → Fin (n ℕ.∸ toℕ j)
+(suc n) ℕ-′ i = n ℕ- i
+
 -- m ℕ-ℕ "i" = m ∸ i.
 
-infixl 6 _ℕ-ℕ_
+infixl 6 _ℕ-ℕ_ _ℕ-ℕ′_
 
 _ℕ-ℕ_ : (n : ℕ) → Fin (suc n) → ℕ
 n     ℕ-ℕ zero   = n
 suc n ℕ-ℕ suc i  = n ℕ-ℕ i
 
+_ℕ-ℕ′_ : (n : ℕ) {{_ : NonZero n}} → Fin n → ℕ
+suc n ℕ-ℕ′ i  = n ℕ-ℕ i
+
 -- pred "i" = "pred i".
 
 pred : Fin n → Fin n
@@ -258,6 +296,10 @@ punchOut {_}     {zero}   {suc j} _   = j
 punchOut {suc _} {suc i}  {zero}  _   = zero
 punchOut {suc _} {suc i}  {suc j} i≢j = suc (punchOut (i≢j ∘ cong suc))
 
+punchOut′ : .{{NonZero n}} →
+           {i j : Fin n} → i ≢ j → Fin (ℕ.pred n)
+punchOut′ {n = suc _} = punchOut
+
 -- The function f(i,j) = if j≥i then j+1 else j
 
 punchIn : Fin (suc n) → Fin n → Fin (suc n)
@@ -265,6 +307,10 @@ punchIn zero    j       = suc j
 punchIn (suc i) zero    = zero
 punchIn (suc i) (suc j) = suc (punchIn i j)
 
+punchIn′ : .{{NonZero n}} →
+          Fin n → Fin (ℕ.pred n) → Fin n
+punchIn′ {n = suc _} = punchIn
+
 -- The function f(i,j) such that f(i,j) = if j≤i then j else j-1
 
 pinch : Fin n → Fin (suc n) → Fin n
@@ -272,6 +318,10 @@ pinch {suc n} _       zero    = zero
 pinch {suc n} zero    (suc j) = j
 pinch {suc n} (suc i) (suc j) = suc (pinch i j)
 
+pinch′ : .{{NonZero n}} →
+        Fin (ℕ.pred n) → Fin n → Fin (ℕ.pred n)
+pinch′ {n = suc _} = pinch
+
 ------------------------------------------------------------------------
 -- Order relations
 
diff --git a/src/Data/Fin/Permutation.agda b/src/Data/Fin/Permutation.agda
index 19292f102d..30885c1e5d 100644
--- a/src/Data/Fin/Permutation.agda
+++ b/src/Data/Fin/Permutation.agda
@@ -145,7 +145,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
   inverseʳ′ : Inverseʳ _≡_ _≡_ to from
   inverseʳ′ j = begin
     from (to j)                                                      ≡⟨⟩
-    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong′ i (cong πˡ (punchIn-punchOut _)) ⟩
+    punchOut {i = i} {πˡ (punchIn (πʳ i) (punchOut to-punchOut))} _  ≡⟨ punchOut-cong-eq i (cong πˡ (punchIn-punchOut _)) ⟩
     punchOut {i = i} {πˡ (πʳ (punchIn i j))}                      _  ≡⟨ punchOut-cong i (inverseˡ π) ⟩
     punchOut {i = i} {punchIn i j}                                _  ≡⟨ punchOut-punchIn i ⟩
     j                                                                ∎
@@ -153,7 +153,7 @@ remove {m} {n} i π = permutation to from inverseˡ′ inverseʳ′
   inverseˡ′ : Inverseˡ _≡_ _≡_ to from
   inverseˡ′ j = begin
     to (from j)                                                       ≡⟨⟩
-    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong′ (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
+    punchOut {i = πʳ i} {πʳ (punchIn i (punchOut from-punchOut))}  _  ≡⟨ punchOut-cong-eq (πʳ i) (cong πʳ (punchIn-punchOut _)) ⟩
     punchOut {i = πʳ i} {πʳ (πˡ (punchIn (πʳ i) j))}               _  ≡⟨ punchOut-cong (πʳ i) (inverseʳ π) ⟩
     punchOut {i = πʳ i} {punchIn (πʳ i) j}                         _  ≡⟨ punchOut-punchIn (πʳ i) ⟩
     j                                                                 ∎
diff --git a/src/Data/Fin/Properties.agda b/src/Data/Fin/Properties.agda
index 3698c066a3..477bd85c0e 100644
--- a/src/Data/Fin/Properties.agda
+++ b/src/Data/Fin/Properties.agda
@@ -17,7 +17,7 @@ open import Data.Bool.Base using (Bool; true; false; not; _∧_; _∨_)
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Fin.Base
 open import Data.Fin.Patterns
-open import Data.Nat.Base as ℕ using (ℕ; zero; suc; s≤s; z≤n; z<s; s<s; _∸_; _^_)
+open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; s≤s; z≤n; z<s; s<s; _∸_; _^_)
 import Data.Nat.Properties as ℕₚ
 open import Data.Nat.Solver
 open import Data.Unit using (⊤; tt)
@@ -199,9 +199,13 @@ fromℕ-toℕ : ∀ (i : Fin n) → fromℕ (toℕ i) ≡ strengthen i
 fromℕ-toℕ zero    = refl
 fromℕ-toℕ (suc i) = cong suc (fromℕ-toℕ i)
 
-≤fromℕ : ∀ (i : Fin (ℕ.suc n)) → i ≤ fromℕ n
+≤fromℕ : ∀ (i : Fin (suc n)) → i ≤ fromℕ n
 ≤fromℕ i = subst (toℕ i ℕ.≤_) (sym (toℕ-fromℕ _)) (toℕ≤pred[n] i)
 
+≤fromℕ′ : .{{NonZero n}} →
+          (i : Fin n) → i ≤ fromℕ (ℕ.pred n)
+≤fromℕ′ {n = suc n} i = ≤fromℕ i
+
 ------------------------------------------------------------------------
 -- fromℕ<
 ------------------------------------------------------------------------
@@ -466,7 +470,7 @@ inject₁ℕ≤ = ℕₚ.<⇒≤ ∘ inject₁ℕ<
 ≤̄⇒inject₁< : i ≤ j → inject₁ i < suc j
 ≤̄⇒inject₁< {i = i} i≤j rewrite sym (toℕ-inject₁ i) = s<s i≤j
 
-ℕ<⇒inject₁< : ∀ {i : Fin (ℕ.suc n)} {j : Fin n} → j < i → inject₁ j < i
+ℕ<⇒inject₁< : ∀ {i : Fin (suc n)} {j : Fin n} → j < i → inject₁ j < i
 ℕ<⇒inject₁< {i = suc i} (s≤s j≤i) = ≤̄⇒inject₁< j≤i
 
 i≤inject₁[j]⇒i≤1+j : i ≤ inject₁ j → i ≤ suc j
@@ -478,9 +482,9 @@ i≤inject₁[j]⇒i≤1+j {i = suc i} {j = suc j} (s≤s i≤j) = s≤s (ℕₚ
 ------------------------------------------------------------------------
 
 toℕ-lower₁ : ∀ i (p : n ≢ toℕ i) → toℕ (lower₁ i p) ≡ toℕ i
-toℕ-lower₁ {ℕ.zero}  zero    p = contradiction refl p
-toℕ-lower₁ {ℕ.suc m} zero    p = refl
-toℕ-lower₁ {ℕ.suc m} (suc i) p = cong ℕ.suc (toℕ-lower₁ i (p ∘ cong ℕ.suc))
+toℕ-lower₁ {zero}  zero    p = contradiction refl p
+toℕ-lower₁ {suc m} zero    p = refl
+toℕ-lower₁ {suc m} (suc i) p = cong suc (toℕ-lower₁ i (p ∘ cong suc))
 
 lower₁-injective : ∀ {n≢i : n ≢ toℕ i} {n≢j : n ≢ toℕ j} →
                    lower₁ i n≢i ≡ lower₁ j n≢j → i ≡ j
@@ -500,6 +504,11 @@ inject₁-lower₁ {suc n} zero     _       = refl
 inject₁-lower₁ {suc n} (suc i)  n+1≢i+1 =
   cong suc (inject₁-lower₁ i  (n+1≢i+1 ∘ cong suc))
 
+inject₁-lower₁′ : .{{_ : NonZero n}} →
+                  (i : Fin n) (n≢i+1 : n ≢ suc (toℕ i)) →
+                  inject₁′ (lower₁′ i n≢i+1) ≡ i
+inject₁-lower₁′ {n = suc n} i n≢i+1 = inject₁-lower₁ i (n≢i+1 ∘ cong suc)
+
 lower₁-inject₁′ : ∀ (i : Fin n) (n≢i : n ≢ toℕ (inject₁ i)) →
                   lower₁ (inject₁ i) n≢i ≡ i
 lower₁-inject₁′ zero    _       = refl
@@ -517,10 +526,21 @@ lower₁-irrelevant {suc n} zero     _   _ = refl
 lower₁-irrelevant {suc n} (suc i)  _   _ =
   cong suc (lower₁-irrelevant i _ _)
 
-inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (ℕ.suc n)} →
+lower₁-irrelevant′ : .{{_ : NonZero n}} →
+                    (i : Fin n) (n≢i₁+1 n≢i₂+1 : n ≢ suc (toℕ i)) →
+                    lower₁′ i n≢i₁+1 ≡ lower₁′ i n≢i₂+1
+lower₁-irrelevant′ {n = suc n} i n≢i₁+1 n≢i₂+1 =
+  lower₁-irrelevant i (n≢i₁+1 ∘ cong suc) (n≢i₂+1 ∘ cong suc)
+
+inject₁≡⇒lower₁≡ : ∀ {i : Fin n} {j : Fin (suc n)} →
                   (n≢j : n ≢ toℕ j) → inject₁ i ≡ j → lower₁ j n≢j ≡ i
 inject₁≡⇒lower₁≡ n≢j i≡j = inject₁-injective (trans (inject₁-lower₁ _ n≢j) (sym i≡j))
 
+inject₁≡⇒lower₁≡′ : .{{_ : NonZero n}} →
+                     {i : Fin (ℕ.pred n)} {j : Fin n} →
+                     (n≢j+1 : n ≢ suc (toℕ j)) → inject₁′ i ≡ j → lower₁′ j n≢j+1 ≡ i
+inject₁≡⇒lower₁≡′ {n = suc n} n≢j+1 = inject₁≡⇒lower₁≡ (n≢j+1 ∘ cong suc)
+
 ------------------------------------------------------------------------
 -- inject≤
 ------------------------------------------------------------------------
@@ -554,6 +574,10 @@ pred< : ∀ (i : Fin (suc n)) → i ≢ zero → pred i < i
 pred< zero    i≢0 = contradiction refl i≢0
 pred< (suc i) _   = ≤̄⇒inject₁< ℕₚ.≤-refl
 
+pred<′ : .{{_ : NonZero n}} →
+        (i : Fin n) → i ≢ zero′ → pred i < i
+pred<′ {n = suc n} i = pred< i
+
 ------------------------------------------------------------------------
 -- splitAt
 ------------------------------------------------------------------------
@@ -831,13 +855,23 @@ punchOut-cong {_}     zero    {suc j} {suc k}            = suc-injective
 punchOut-cong {suc n} (suc i) {zero}  {zero}   _ = refl
 punchOut-cong {suc n} (suc i) {suc j} {suc k}    = cong suc ∘ punchOut-cong i ∘ suc-injective
 
+punchOut-cong′ : .{{_ : NonZero n}} →
+                 ∀ (i : Fin n) {j k} {i≢j : i ≢ j} {i≢k : i ≢ k} →
+                 j ≡ k → punchOut′ i≢j ≡ punchOut′ i≢k
+punchOut-cong′ {n = suc n} = punchOut-cong
+
 -- An alternative to 'punchOut-cong' in the which the new inequality argument is
 -- specific. Useful for enabling the omission of that argument during equational
 -- reasoning.
 
-punchOut-cong′ : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
+punchOut-cong-eq : ∀ (i : Fin (suc n)) {j k} {p : i ≢ j} (q : j ≡ k) →
                  punchOut p ≡ punchOut (p ∘ sym ∘ trans q ∘ sym)
-punchOut-cong′ i q = punchOut-cong i q
+punchOut-cong-eq i q = punchOut-cong i q
+
+punchOut-cong-eq′ : .{{_ : NonZero n}} →
+                   ∀ (i : Fin n) {j k} {p : i ≢ j} (q : j ≡ k) →
+                   punchOut′ p ≡ punchOut′ (p ∘ sym ∘ trans q ∘ sym)
+punchOut-cong-eq′ {n = suc n} = punchOut-cong-eq
 
 punchOut-injective : ∀ {i j k : Fin (suc n)}
                      (i≢j : i ≢ j) (i≢k : i ≢ k) →
@@ -849,6 +883,11 @@ punchOut-injective {suc n} {suc i}  {zero}  {zero}  _   _    _    = refl
 punchOut-injective {suc n} {suc i}  {suc j} {suc k} i≢j i≢k pⱼ≡pₖ =
   cong suc (punchOut-injective (i≢j ∘ cong suc) (i≢k ∘ cong suc) (suc-injective pⱼ≡pₖ))
 
+punchOut-injective′ : .{{_ : NonZero n}} →
+                     {i j k : Fin n} (i≢j : i ≢ j) (i≢k : i ≢ k) →
+                     punchOut′ i≢j ≡ punchOut′ i≢k → j ≡ k
+punchOut-injective′ {n = suc n} = punchOut-injective
+
 punchIn-punchOut : ∀ {i j : Fin (suc n)} (i≢j : i ≢ j) →
                    punchIn i (punchOut i≢j) ≡ j
 punchIn-punchOut {_}     {zero}   {zero}  0≢0 = contradiction refl 0≢0
@@ -857,6 +896,11 @@ punchIn-punchOut {suc m} {suc i}  {zero}  i≢j = refl
 punchIn-punchOut {suc m} {suc i}  {suc j} i≢j =
   cong suc (punchIn-punchOut (i≢j ∘ cong suc))
 
+punchIn-punchOut′ : .{{_ : NonZero n}} →
+                   {i j : Fin n} (i≢j : i ≢ j) →
+                   punchIn′ i (punchOut′ i≢j) ≡ j
+punchIn-punchOut′ {n = suc n} = punchIn-punchOut
+
 punchOut-punchIn : ∀ i {j : Fin n} → punchOut {i = i} {j = punchIn i j} (punchInᵢ≢i i j ∘ sym) ≡ j
 punchOut-punchIn zero    {j}     = refl
 punchOut-punchIn (suc i) {zero}  = refl
@@ -882,7 +926,7 @@ pinch-mono-≤ 0F      {suc j} {suc k} (s≤s j≤k) = j≤k
 pinch-mono-≤ (suc i) {0F}    {k}     0≤n       = z≤n
 pinch-mono-≤ (suc i) {suc j} {suc k} (s≤s j≤k) = s≤s (pinch-mono-≤ i j≤k)
 
-pinch-injective : ∀ {i : Fin n} {j k : Fin (ℕ.suc n)} →
+pinch-injective : ∀ {i : Fin n} {j k : Fin (suc n)} →
                   suc i ≢ j → suc i ≢ k → pinch i j ≡ pinch i k → j ≡ k
 pinch-injective {i = i}     {zero}  {zero}  _     _     _  = refl
 pinch-injective {i = zero}  {zero}  {suc k} _     1+i≢k eq =
@@ -896,6 +940,11 @@ pinch-injective {i = suc i} {suc j} {suc k} 1+i≢j 1+i≢k eq =
     (pinch-injective (1+i≢j ∘ cong suc) (1+i≢k ∘ cong suc)
       (suc-injective eq))
 
+pinch-injective′ : .{{_ : NonZero n}} →
+                  {i : Fin (ℕ.pred n)} {j k : Fin n} →
+                  suc′ i ≢ j → suc′ i ≢ k → pinch′ i j ≡ pinch′ i k → j ≡ k
+pinch-injective′ {n = suc n} = pinch-injective
+
 ------------------------------------------------------------------------
 -- Quantification
 ------------------------------------------------------------------------
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 5bc11aeef1..b2724adf9c 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -23,7 +23,7 @@ open import Data.List.Relation.Unary.All using (All; []; _∷_)
 open import Data.List.Relation.Unary.Any using (Any; here; there)
 open import Data.Maybe.Base using (Maybe; just; nothing)
 open import Data.Nat.Base
-open import Data.Nat.Divisibility
+open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
 open import Data.Product as Prod hiding (map; zip)
 import Data.Product.Relation.Unary.All as Prod using (All)
@@ -673,10 +673,10 @@ tabulate-lookup : ∀ (xs : List A) → tabulate (lookup xs) ≡ xs
 tabulate-lookup []       = refl
 tabulate-lookup (x ∷ xs) = cong (_ ∷_) (tabulate-lookup xs)
 
-length-tabulate : ∀ {n} → (f : Fin n → A) →
+length-tabulate : ∀ {n} (f : Fin n → A) →
                   length (tabulate f) ≡ n
 length-tabulate {n = zero} f = refl
-length-tabulate {n = suc n} f = cong suc (length-tabulate (λ z → f (suc z)))
+length-tabulate {n = suc n} f = cong suc (length-tabulate (f ∘ suc))
 
 lookup-tabulate : ∀ {n} → (f : Fin n → A) →
                   ∀ i → let i′ = cast (sym (length-tabulate f)) i
diff --git a/src/Data/Vec/Base.agda b/src/Data/Vec/Base.agda
index d25c2384c8..450d01675f 100644
--- a/src/Data/Vec/Base.agda
+++ b/src/Data/Vec/Base.agda
@@ -53,9 +53,15 @@ length {n = n} _ = n
 head : Vec A (1 + n) → A
 head (x ∷ xs) = x
 
+head′ : .{{_ : NonZero n}} → Vec A n → A
+head′ {n = suc n} = head
+
 tail : Vec A (1 + n) → Vec A n
 tail (x ∷ xs) = xs
 
+tail′ : .{{_ : NonZero n}} → Vec A n → Vec A (pred n)
+tail′ {n = suc n} = tail
+
 lookup : Vec A n → Fin n → A
 lookup (x ∷ xs) zero    = x
 lookup (x ∷ xs) (suc i) = lookup xs i
@@ -68,10 +74,18 @@ insert : Vec A n → Fin (suc n) → A → Vec A (suc n)
 insert xs       zero     v = v ∷ xs
 insert (x ∷ xs) (suc i)  v = x ∷ insert xs i v
 
+insert′ : .{{_ : NonZero n}} →
+         Vec A (pred n) → Fin n → A → Vec A n
+insert′ {n = suc n} = insert
+
 remove : Vec A (suc n) → Fin (suc n) → Vec A n
 remove (_ ∷ xs)     zero     = xs
 remove (x ∷ y ∷ xs) (suc i)  = x ∷ remove (y ∷ xs) i
 
+remove′ : .{{_ : NonZero n}} →
+         Vec A n → Fin n → Vec A (pred n)
+remove′ {n = suc n} = remove
+
 updateAt : Fin n → (A → A) → Vec A n → Vec A n
 updateAt zero    f (x ∷ xs) = f x ∷ xs
 updateAt (suc i) f (x ∷ xs) = x   ∷ updateAt i f xs
@@ -290,6 +304,9 @@ split (x ∷ y ∷ xs) = Prod.map (x ∷_) (y ∷_) (split xs)
 uncons : Vec A (suc n) → A × Vec A n
 uncons (x ∷ xs) = x , xs
 
+uncons′ : .{{NonZero n}} → Vec A n → A × Vec A (pred n)
+uncons′ {n = suc n} = uncons
+
 ------------------------------------------------------------------------
 -- Operations involving ≤
 
@@ -348,10 +365,16 @@ init : Vec A (1 + n) → Vec A n
 init xs with initLast xs
 ... | (ys , y , refl) = ys
 
+init′ : .{{NonZero n}} → (xs : Vec A n) → Vec A (pred n)
+init′ {n = suc n} = init
+
 last : Vec A (1 + n) → A
 last xs with initLast xs
 ... | (ys , y , refl) = y
 
+last′ : .{{NonZero n}} → (xs : Vec A n) → A
+last′ {n = suc n} = last
+
 ------------------------------------------------------------------------
 -- Other operations
 
diff --git a/src/Data/Vec/Functional.agda b/src/Data/Vec/Functional.agda
index 1696e6b482..fd4e683797 100644
--- a/src/Data/Vec/Functional.agda
+++ b/src/Data/Vec/Functional.agda
@@ -15,7 +15,7 @@
 
 module Data.Vec.Functional where
 
-open import Data.Fin.Base
+open import Data.Fin.Base hiding (pred)
 open import Data.List.Base as L using (List)
 open import Data.Nat.Base as ℕ using (ℕ; zero; suc; NonZero; pred)
 open import Data.Product using (Σ; ∃; _×_; _,_; proj₁; proj₂; uncurry)
@@ -72,12 +72,21 @@ length {n = n} _ = n
 head : ∀ {n} → Vector A (suc n) → A
 head xs = xs zero
 
+head′ : ∀ {n} {{_ : NonZero n}} → Vector A n → A
+head′ {n = suc n} = head
+
 tail : ∀ {n} → Vector A (suc n) → Vector A n
 tail xs = xs ∘ suc
 
+tail′ : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n)
+tail′ {n = suc n} = tail
+
 uncons : ∀ {n} → Vector A (suc n) → A × Vector A n
 uncons xs = head xs , tail xs
 
+uncons′ : ∀ {n} {{_ : NonZero n}} → Vector A n → A × Vector A (pred n)
+uncons′ {n = suc n} = uncons
+
 replicate : ∀ {n} → A → Vector A n
 replicate = const
 
@@ -90,6 +99,10 @@ insert {n = suc n} xs (suc i) v (suc j) = insert (tail xs) i v j
 remove : ∀ {n} → Fin (suc n) → Vector A (suc n) → Vector A n
 remove i t = t ∘ punchIn i
 
+remove′ : ∀ {n} .{{_ : NonZero n}} →
+         Fin n → Vector A n → Vector A (pred n)
+remove′ {n = suc n} i t = t ∘ punchIn′ i
+
 updateAt : ∀ {n} → Fin n → (A → A) → Vector A n → Vector A n
 updateAt {n = suc n} zero    f xs zero    = f (head xs)
 updateAt {n = suc n} zero    f xs (suc j) = xs (suc j)
@@ -149,8 +162,14 @@ reverse xs = xs ∘ opposite
 init : ∀ {n} → Vector A (suc n) → Vector A n
 init xs = xs ∘ inject₁
 
+init′ : ∀ {n} {{_ : NonZero n}} → Vector A n → Vector A (pred n)
+init′ {n = suc n} = init
+
 last : ∀ {n} → Vector A (suc n) → A
 last {n = n} xs = xs (fromℕ n)
 
+last′ : ∀ {n} {{_ : NonZero n}} → Vector A n → A
+last′ {n = suc n} = last
+
 transpose : ∀ {m n} → Vector (Vector A n) m → Vector (Vector A m) n
 transpose = flip
diff --git a/src/Data/Vec/Properties.agda b/src/Data/Vec/Properties.agda
index 805570c42e..ceb3ccba6e 100644
--- a/src/Data/Vec/Properties.agda
+++ b/src/Data/Vec/Properties.agda
@@ -10,7 +10,8 @@ module Data.Vec.Properties where
 
 open import Algebra.Definitions
 open import Data.Bool.Base using (true; false)
-open import Data.Fin.Base as Fin using (Fin; zero; suc; toℕ; fromℕ<; _↑ˡ_; _↑ʳ_)
+open import Data.Fin.Base as Fin
+  using (Fin; zero; suc; toℕ; _↑ˡ_; _↑ʳ_; combine)
 open import Data.List.Base as List using (List)
 open import Data.Nat.Base
 open import Data.Nat.Properties
@@ -533,12 +534,12 @@ lookup-cast₂ eq (_ ∷ xs) (suc i) =
   lookup-cast₂ (suc-injective eq) xs i
 
 lookup-concat : ∀ (xss : Vec (Vec A m) n) i j →
-                lookup (concat xss) (Fin.combine i j) ≡ lookup (lookup xss i) j
+                lookup (concat xss) (combine i j) ≡ lookup (lookup xss i) j
 lookup-concat (xs ∷ xss) zero j = lookup-++ˡ xs (concat xss) j
 lookup-concat (xs ∷ xss) (suc i) j = begin
-  lookup (concat (xs ∷ xss)) (Fin.combine (suc i) j)
-    ≡⟨ lookup-++ʳ xs (concat xss) (Fin.combine i j) ⟩
-  lookup (concat xss) (Fin.combine i j)
+  lookup (concat (xs ∷ xss)) (combine (suc i) j)
+    ≡⟨ lookup-++ʳ xs (concat xss) (combine i j) ⟩
+  lookup (concat xss) (combine i j)
     ≡⟨ lookup-concat xss i j ⟩
   lookup (lookup (xs ∷ xss) (suc i)) j
     ∎ where open ≡-Reasoning
@@ -746,9 +747,9 @@ zipWith-is-⊛ f (x ∷ xs) (y ∷ ys) = cong (_ ∷_) (zipWith-is-⊛ f xs ys)
 -- _⊛*_
 
 lookup-⊛* : ∀ (fs : Vec (A → B) m) (xs : Vec A n) i j →
-            lookup (fs ⊛* xs) (Fin.combine i j) ≡ (lookup fs i $ lookup xs j)
+            lookup (fs ⊛* xs) (combine i j) ≡ (lookup fs i $ lookup xs j)
 lookup-⊛* (f ∷ fs) xs zero j = trans (lookup-++ˡ (map f xs) _ j) (lookup-map j f xs)
-lookup-⊛* (f ∷ fs) xs (suc i) j = trans (lookup-++ʳ (map f xs) _ (Fin.combine i j)) (lookup-⊛* fs xs i j)
+lookup-⊛* (f ∷ fs) xs (suc i) j = trans (lookup-++ʳ (map f xs) _ (combine i j)) (lookup-⊛* fs xs i j)
 
 ------------------------------------------------------------------------
 -- foldl
@@ -1065,12 +1066,22 @@ insert-lookup : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) →
 insert-lookup xs       zero     v = refl
 insert-lookup (x ∷ xs) (suc i)  v = insert-lookup xs i v
 
+insert-lookup′ : .{{_ : NonZero n}} →
+                (xs : Vec A (pred n)) (i : Fin n) (v : A) →
+                lookup (insert′ xs i v) i ≡ v
+insert-lookup′ {n = suc n} = insert-lookup
+
 insert-punchIn : ∀ (xs : Vec A n) (i : Fin (suc n)) (v : A) (j : Fin n) →
                  lookup (insert xs i v) (Fin.punchIn i j) ≡ lookup xs j
 insert-punchIn xs       zero     v j       = refl
 insert-punchIn (x ∷ xs) (suc i)  v zero    = refl
 insert-punchIn (x ∷ xs) (suc i)  v (suc j) = insert-punchIn xs i v j
 
+insert-punchIn′ : .{{_ : NonZero n}} →
+                 (xs : Vec A (pred n)) (i : Fin n) (v : A) (j : Fin (pred n)) →
+                 lookup (insert′ xs i v) (Fin.punchIn′ i j) ≡ lookup xs j
+insert-punchIn′ {n = suc n} = insert-punchIn
+
 remove-punchOut : ∀ (xs : Vec A (suc n)) {i} {j} (i≢j : i ≢ j) →
                   lookup (remove xs i) (Fin.punchOut i≢j) ≡ lookup xs j
 remove-punchOut (x ∷ xs)     {zero}  {zero}  i≢j = contradiction refl i≢j
@@ -1079,6 +1090,11 @@ remove-punchOut (x ∷ y ∷ xs) {suc i} {zero}  i≢j = refl
 remove-punchOut (x ∷ y ∷ xs) {suc i} {suc j} i≢j =
   remove-punchOut (y ∷ xs) (i≢j ∘ cong suc)
 
+remove-punchOut′ : .{{_ : NonZero n}} →
+                  ∀ (xs : Vec A n) {i} {j} (i≢j : i ≢ j) →
+                  lookup (remove′ xs i) (Fin.punchOut′ i≢j) ≡ lookup xs j
+remove-punchOut′ {n = suc n} = remove-punchOut
+
 ------------------------------------------------------------------------
 -- remove
 
@@ -1089,12 +1105,22 @@ remove-insert (x ∷ xs)     (suc zero)     v = refl
 remove-insert (x ∷ y ∷ xs) (suc (suc i))  v =
   cong (x ∷_) (remove-insert (y ∷ xs) (suc i) v)
 
+remove-insert′ : .{{_ : NonZero n}} →
+                (xs : Vec A (pred n)) (i : Fin n) (v : A) →
+                remove′ (insert′ xs i v) i ≡ xs
+remove-insert′ {n = suc n} = remove-insert
+
 insert-remove : ∀ (xs : Vec A (suc n)) (i : Fin (suc n)) →
                 insert (remove xs i) i (lookup xs i) ≡ xs
 insert-remove (x ∷ xs)     zero     = refl
 insert-remove (x ∷ y ∷ xs) (suc i)  =
   cong (x ∷_) (insert-remove (y ∷ xs) i)
 
+insert-remove′ : .{{_ : NonZero n}} →
+                (xs : Vec A n) (i : Fin n) →
+                insert′ (remove′ xs i) i (lookup xs i) ≡ xs
+insert-remove′ {n = suc n} = insert-remove
+
 ------------------------------------------------------------------------
 -- Conversion function
 
diff --git a/src/Data/Vec/Recursive.agda b/src/Data/Vec/Recursive.agda
index b30089d33c..60ed69b9ae 100644
--- a/src/Data/Vec/Recursive.agda
+++ b/src/Data/Vec/Recursive.agda
@@ -74,12 +74,21 @@ uncons : ∀ n → A ^ suc n → A × A ^ n
 uncons 0        a        = a , lift tt
 uncons (suc n)  (a , as) = a , as
 
+uncons′ : ∀ n → .{{_ : NonZero n}} → A ^ n → A × A ^ (pred n)
+uncons′ (suc n) = uncons n
+
 head : ∀ n → A ^ suc n → A
 head n as = proj₁ (uncons n as)
 
+head′ : ∀ n → .{{_ : NonZero n}} → A ^ n → A
+head′ (suc n) = head n
+
 tail : ∀ n → A ^ suc n → A ^ n
 tail n as = proj₂ (uncons n as)
 
+tail′ : ∀ n → .{{_ : NonZero n}} → A ^ n → A ^ (pred n)
+tail′ (suc n) = tail n
+
 fromVec : ∀[ Vec A ⇒ (A ^_) ]
 fromVec = Vec.foldr (_ ^_) (cons _) _
 
diff --git a/src/Data/Vec/Relation/Unary/All.agda b/src/Data/Vec/Relation/Unary/All.agda
index b16340ef6b..9184f4e273 100644
--- a/src/Data/Vec/Relation/Unary/All.agda
+++ b/src/Data/Vec/Relation/Unary/All.agda
@@ -52,9 +52,15 @@ data All {A : Set a} (P : Pred A p) : Vec A n → Set (p ⊔ a) where
 head : All P (x ∷ xs) → P x
 head (px ∷ pxs) = px
 
+head′ : .{{_ : NonZero n}} → All P xs → P (Vec.head′ {n = n} xs)
+head′ {n = suc _} pxs@(_ ∷ _) = head pxs
+
 tail : All P (x ∷ xs) → All P xs
 tail (px ∷ pxs) = pxs
 
+tail′ : .{{_ : NonZero n}} → All P xs → All P (Vec.tail′ {n = n} xs)
+tail′ {n = suc _} pxs@(_ ∷ _) = tail pxs
+
 reduce : (f : ∀ {x} → P x → B) → ∀ {n} {xs : Vec A n} → All P xs → Vec B n
 reduce f []         = []
 reduce f (px ∷ pxs) = f px ∷ reduce f pxs
@@ -62,6 +68,10 @@ reduce f (px ∷ pxs) = f px ∷ reduce f pxs
 uncons : All P (x ∷ xs) → P x × All P xs
 uncons = < head , tail >
 
+uncons′ : .{{_ : NonZero n}} →
+          All P xs → P (Vec.head′ {n = n} xs) × All P (Vec.tail′ {n = n} xs)
+uncons′ = < head′ , tail′ >
+
 map : P ⊆ Q → All P ⊆ All Q {n}
 map g []         = []
 map g (px ∷ pxs) = g px ∷ map g pxs
diff --git a/src/Data/Vec/Relation/Unary/Any.agda b/src/Data/Vec/Relation/Unary/Any.agda
index a54991976f..831df9f08d 100644
--- a/src/Data/Vec/Relation/Unary/Any.agda
+++ b/src/Data/Vec/Relation/Unary/Any.agda
@@ -44,11 +44,19 @@ head : ∀ {x} → ¬ Any P xs → Any P (x ∷ xs) → P x
 head ¬pxs (here px)   = px
 head ¬pxs (there pxs) = contradiction pxs ¬pxs
 
+head′ : .{{_ : NonZero n}} →
+        ¬ Any P (Vec.tail′ {n = n} xs) → Any P xs → P (Vec.head′ {n = n} xs)
+head′ {n = suc _} {xs = _ ∷ _} ¬pxs = head ¬pxs
+
 -- If the head does not satisfy the predicate, then the tail will.
 tail : ∀ {x} → ¬ P x → Any P (x ∷ xs) → Any P xs
 tail ¬px (here  px)  = ⊥-elim (¬px px)
 tail ¬px (there pxs) = pxs
 
+tail′ : .{{_ : NonZero n}} →
+        ¬ P (Vec.head′ {n = n} xs) → Any P xs → Any P (Vec.tail′ {n = n} xs)
+tail′ {n = suc _} {xs = _ ∷ _} ¬px = tail ¬px
+
 -- Convert back and forth with sum
 toSum : ∀ {x} → Any P (x ∷ xs) → P x ⊎ Any P xs
 toSum (here px)   = inj₁ px
diff --git a/src/Data/Vec/Relation/Unary/Linked/Properties.agda b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
index 3935a263c4..3ebe0eb19f 100644
--- a/src/Data/Vec/Relation/Unary/Linked/Properties.agda
+++ b/src/Data/Vec/Relation/Unary/Linked/Properties.agda
@@ -43,6 +43,11 @@ module _ (trans : Transitive R) where
   Linked⇒All Rvx [-]         = Rvx ∷ []
   Linked⇒All Rvx (Rxy ∷ Rxs) = Rvx ∷ Linked⇒All (trans Rvx Rxy) Rxs
 
+  Linked⇒All′ : .{{_ : NonZero n}} →
+                ∀ {v} {xs : Vec _ n} → R v (head′ xs) →
+                Linked R xs → All (R v) xs
+  Linked⇒All′ {n = suc n} = Linked⇒All {n = n}
+
   lookup⁺ : ∀ {i j} {xs : Vec _ n} →
            Linked R xs → i < j →
            R (lookup xs i) (lookup xs j)