From a044edd81bd2f664967a4a5c0325a4e5915ab1d9 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Wed, 14 Jun 2023 13:54:03 -0400
Subject: [PATCH 1/9] Added functions take-drop-1 and take-one-more to stdl
 Data.List.Properties

Names of those functions are up to debate
---
 src/Data/List/Properties.agda | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 312ef2e7a8..286b7f9f28 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -758,6 +758,10 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
+take-one-more : {ℓ : Level} {X : Set ℓ} {m : ℕ} (x : Fin m) (f : Fin m → X) →
+   take (toℕ x) (tabulate f) ∷ʳ f x ≡ take (suc (toℕ x)) (tabulate f)
+take-one-more {m = suc m} zero    f = refl
+take-one-more {m = suc m} (suc x) f = cong (f zero ∷_) (take-one-more x (f ∘ suc))
 ------------------------------------------------------------------------
 -- drop
 
@@ -766,11 +770,20 @@ length-drop zero    xs       = refl
 length-drop (suc n) []       = refl
 length-drop (suc n) (x ∷ xs) = length-drop n xs
 
+------------------------------------------------------------------------
+-- take-drop
+
 take++drop : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
 take++drop zero    xs       = refl
 take++drop (suc n) []       = refl
 take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
 
+take-drop-1 : {x : Level} {X : Set x} {k : ℕ} (f : Fin k → X) (n : Fin k) →
+  drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
+take-drop-1 f zero    = refl
+take-drop-1 f (suc n) = take-drop-1 (f ∘ suc) n
+
+
 ------------------------------------------------------------------------
 -- splitAt
 
@@ -1075,6 +1088,8 @@ module _ {x y : A} where
 ∷ʳ-++ : ∀ (xs : List A) (a : A) (ys : List A) → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
 ∷ʳ-++ xs a ys = ++-assoc xs [ a ] ys
 
+
+
 ------------------------------------------------------------------------
 -- DEPRECATED
 ------------------------------------------------------------------------

From ddea1700a5565e4f10c1eb656ba920a894c3503b Mon Sep 17 00:00:00 2001
From: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com>
Date: Wed, 14 Jun 2023 14:03:17 -0400
Subject: [PATCH 2/9] Update CHANGELOG.md

Add functions :
   take-drop-1
   take-one-more
to stdl Data.List.Propreties
---
 CHANGELOG.md | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d5ba31beaf..71e658569c 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2784,7 +2784,12 @@ Other minor changes
   foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs
   foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs
   ```
-
+* Added new functions to `Data.List.Properties`
+  ```agda
+  take-drop-1 : {x : Level} {X : Set x} {k : ℕ} (f : Fin k → X) (n : Fin k) → drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
+  take-one-more : {ℓ : Level} {X : Set ℓ} {m : ℕ} (x : Fin m) (f : Fin m → X) → take (toℕ x) (tabulate f) ∷ʳ f x ≡ take (suc (toℕ x)) (tabulate f)
+  ```
+  
 NonZero/Positive/Negative changes
 ---------------------------------
 

From d7966f580ac2fad5d95b55d312b989821f920a57 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Thu, 15 Jun 2023 15:00:30 -0400
Subject: [PATCH 3/9] Rename of 2 new functions of take and drop in
 Data.List.Properties

`take-one-more` to `take-suc-tabulate`
`take-drop-1` to `take-tabulate-1`

`take-tabulate-1` is now with other `take` functions
---
 src/Data/List/Properties.agda | 23 ++++++++++-------------
 1 file changed, 10 insertions(+), 13 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 286b7f9f28..1e5dfdf0e3 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -758,10 +758,16 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
-take-one-more : {ℓ : Level} {X : Set ℓ} {m : ℕ} (x : Fin m) (f : Fin m → X) →
-   take (toℕ x) (tabulate f) ∷ʳ f x ≡ take (suc (toℕ x)) (tabulate f)
-take-one-more {m = suc m} zero    f = refl
-take-one-more {m = suc m} (suc x) f = cong (f zero ∷_) (take-one-more x (f ∘ suc))
+take-suc-tabulate :  {m : ℕ} (n : Fin m) (f : Fin m → A) →
+   take (toℕ n) (tabulate f) ∷ʳ f n ≡ take (suc (toℕ n)) (tabulate f)
+take-suc-tabulate {m = suc m} zero    f = refl
+take-suc-tabulate {m = suc m} (suc n) f = cong (f zero ∷_) (take-suc-tabulate n (f ∘ suc))
+
+take-tabulate-1 : {m : ℕ} (f : Fin m → A) (n : Fin m) →
+  drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
+take-tabulate-1 f zero    = refl
+take-tabulate-1 f (suc n) = take-tabulate-1 (f ∘ suc) n
+
 ------------------------------------------------------------------------
 -- drop
 
@@ -770,20 +776,11 @@ length-drop zero    xs       = refl
 length-drop (suc n) []       = refl
 length-drop (suc n) (x ∷ xs) = length-drop n xs
 
-------------------------------------------------------------------------
--- take-drop
-
 take++drop : ∀ n (xs : List A) → take n xs ++ drop n xs ≡ xs
 take++drop zero    xs       = refl
 take++drop (suc n) []       = refl
 take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
 
-take-drop-1 : {x : Level} {X : Set x} {k : ℕ} (f : Fin k → X) (n : Fin k) →
-  drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
-take-drop-1 f zero    = refl
-take-drop-1 f (suc n) = take-drop-1 (f ∘ suc) n
-
-
 ------------------------------------------------------------------------
 -- splitAt
 

From f6f818fb62f1cfe58831dfc70027604ef87df014 Mon Sep 17 00:00:00 2001
From: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com>
Date: Thu, 15 Jun 2023 15:36:51 -0400
Subject: [PATCH 4/9] Update CHANGELOG.md

Added `take-tabulate-1` and `take-suc-tabulate` to Data.List.Properties
---
 CHANGELOG.md | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 71e658569c..938f9586ce 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2053,6 +2053,9 @@ Other minor changes
 
   length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
   length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
+  
+  take-tabulate-1 :(f : Fin m → A) (n : Fin m) → drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
+  take-suc-tabulate :(n : Fin m) (f : Fin m → A) → take (toℕ x) (tabulate f) ∷ʳ f x ≡ take (suc (toℕ x)) (tabulate f)
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
@@ -2784,11 +2787,6 @@ Other minor changes
   foldr-map : foldr f x (map g xs) ≡ foldr (g -⟨ f ∣) x xs
   foldl-map : foldl f x (map g xs) ≡ foldl (∣ f ⟩- g) x xs
   ```
-* Added new functions to `Data.List.Properties`
-  ```agda
-  take-drop-1 : {x : Level} {X : Set x} {k : ℕ} (f : Fin k → X) (n : Fin k) → drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
-  take-one-more : {ℓ : Level} {X : Set ℓ} {m : ℕ} (x : Fin m) (f : Fin m → X) → take (toℕ x) (tabulate f) ∷ʳ f x ≡ take (suc (toℕ x)) (tabulate f)
-  ```
   
 NonZero/Positive/Negative changes
 ---------------------------------

From 7755eddb2406c60c51c8a528a7459ce0cb3931e1 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Thu, 15 Jun 2023 15:54:34 -0400
Subject: [PATCH 5/9] reverse the equality in take-suc-tabulate

---
 CHANGELOG.md                  | 2 +-
 src/Data/List/Properties.agda | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 938f9586ce..d75950f442 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2055,7 +2055,7 @@ Other minor changes
   length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
   
   take-tabulate-1 :(f : Fin m → A) (n : Fin m) → drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
-  take-suc-tabulate :(n : Fin m) (f : Fin m → A) → take (toℕ x) (tabulate f) ∷ʳ f x ≡ take (suc (toℕ x)) (tabulate f)
+  take-suc-tabulate : (n : Fin m) (f : Fin m → A) → take (suc (toℕ n)) (tabulate f) ≡ take (toℕ n) (tabulate f) ∷ʳ f n 
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 1e5dfdf0e3..a37b051fa6 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -759,7 +759,7 @@ length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
 take-suc-tabulate :  {m : ℕ} (n : Fin m) (f : Fin m → A) →
-   take (toℕ n) (tabulate f) ∷ʳ f n ≡ take (suc (toℕ n)) (tabulate f)
+  take (suc (toℕ n)) (tabulate f) ≡ take (toℕ n) (tabulate f) ∷ʳ f n
 take-suc-tabulate {m = suc m} zero    f = refl
 take-suc-tabulate {m = suc m} (suc n) f = cong (f zero ∷_) (take-suc-tabulate n (f ∘ suc))
 

From aa5b8fd9033f3baceab1237a397a308459181249 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Mon, 19 Jun 2023 17:04:19 -0400
Subject: [PATCH 6/9] rewritting of functions of `take-one-more` and
 `take-dorp-1` using `cast` instead of `subst`

separation f each function into two function
`take-one-more` replaced by `take-suc`+ `take-suc-tabulate`
`take-drop-1` replaced by `drop-take-suc`+`drop-take-suc-tabulate`
---
 src/Data/List/Properties.agda | 28 +++++++++++++++++++---------
 1 file changed, 19 insertions(+), 9 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index a37b051fa6..e72fc0ca3f 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -29,6 +29,7 @@ open import Data.Product as Prod hiding (map; zip)
 import Data.Product.Relation.Unary.All as Prod using (All)
 open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
 open import Data.These.Base as These using (These; this; that; these)
+open import Data.Fin.Properties using (toℕ-cast)
 open import Function
 open import Level using (Level)
 open import Relation.Binary as B using (DecidableEquality)
@@ -758,16 +759,15 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
-take-suc-tabulate :  {m : ℕ} (n : Fin m) (f : Fin m → A) →
-  take (suc (toℕ n)) (tabulate f) ≡ take (toℕ n) (tabulate f) ∷ʳ f n
-take-suc-tabulate {m = suc m} zero    f = refl
-take-suc-tabulate {m = suc m} (suc n) f = cong (f zero ∷_) (take-suc-tabulate n (f ∘ suc))
-
-take-tabulate-1 : {m : ℕ} (f : Fin m → A) (n : Fin m) →
-  drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
-take-tabulate-1 f zero    = refl
-take-tabulate-1 f (suc n) = take-tabulate-1 (f ∘ suc) n
+take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
+           take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
+take-suc (x ∷ xs) zero    = refl
+take-suc (x ∷ xs) (suc i) = cong (x ∷_) (take-suc xs i)
 
+take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
+                    take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
+take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
+  = take-suc (tabulate f) (cast _ i)
 ------------------------------------------------------------------------
 -- drop
 
@@ -781,6 +781,16 @@ take++drop zero    xs       = refl
 take++drop (suc n) []       = refl
 take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
 
+drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
+           drop m (take (suc m) xs) ≡ [ lookup xs i ]
+drop-take-suc (x ∷ xs) zero    = refl
+drop-take-suc (x ∷ xs) (suc i) = drop-take-suc xs i
+
+drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
+                  drop m (take (suc m) (tabulate f)) ≡ [ f i ]
+drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
+  = drop-take-suc (tabulate f) (cast _ i)
+
 ------------------------------------------------------------------------
 -- splitAt
 

From 068488d26f7e6770f3b427cb3a86a74e3e97aecf Mon Sep 17 00:00:00 2001
From: Sofia El Boufi--Crouzet <136095087+Sofia-Insa@users.noreply.github.com>
Date: Mon, 19 Jun 2023 17:30:29 -0400
Subject: [PATCH 7/9] Update CHANGELOG.md

update corresponding to rewritte of `take-one-more` and `take-drop-1`
---
 CHANGELOG.md | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d75950f442..da083ffb98 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2053,9 +2053,12 @@ Other minor changes
 
   length-isMagmaHomomorphism : (A : Set a) → IsMagmaHomomorphism (++-rawMagma A) +-rawMagma length
   length-isMonoidHomomorphism : (A : Set a) → IsMonoidHomomorphism (++-[]-rawMonoid A) +-0-rawMonoid length
+
+  take-suc : (o : Fin (length xs)) → let m = toℕ o in take (suc m) xs ≡ take m xs ∷ʳ lookup xs o
+  take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o
+  drop-take-suc : (o : Fin (length xs)) → let m = toℕ o in drop m (take (suc m) xs) ≡ [ lookup xs o ]
+  drop-take-suc-tabulate : (f : Fin n → A) (o : Fin n) → let m = toℕ o in drop m (take (suc m) (tabulate f)) ≡ [ f o ]
   
-  take-tabulate-1 :(f : Fin m → A) (n : Fin m) → drop (toℕ n) (take (suc (toℕ n)) (tabulate f)) ≡ [ f n ]
-  take-suc-tabulate : (n : Fin m) (f : Fin m → A) → take (suc (toℕ n)) (tabulate f) ≡ take (toℕ n) (tabulate f) ∷ʳ f n 
   ```
 
 * Added new patterns and definitions to `Data.Nat.Base`:

From 63a33ea29e85fd4c118a8e7b45c593be2986a2d7 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Mon, 19 Jun 2023 17:31:02 -0400
Subject: [PATCH 8/9] small syntaxe modification

---
 src/Data/List/Properties.agda | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index e72fc0ca3f..b8b4a60aa0 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -759,15 +759,15 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
-           take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
+take-suc : (xs : List A) (o : Fin (length xs)) → let m = toℕ o in
+           take (suc m) xs ≡ take m xs ∷ʳ lookup xs o
 take-suc (x ∷ xs) zero    = refl
-take-suc (x ∷ xs) (suc i) = cong (x ∷_) (take-suc xs i)
+take-suc (x ∷ xs) (suc o) = cong (x ∷_) (take-suc xs o)
 
-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
-                    take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
-  = take-suc (tabulate f) (cast _ i)
+take-suc-tabulate : ∀ {n} (f : Fin n → A) (o : Fin n) → let m = toℕ o in
+                    take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o
+take-suc-tabulate f o rewrite sym (toℕ-cast (sym (length-tabulate f)) o) | sym (lookup-tabulate f o)
+  = take-suc (tabulate f) (cast _ o)
 ------------------------------------------------------------------------
 -- drop
 
@@ -781,15 +781,15 @@ take++drop zero    xs       = refl
 take++drop (suc n) []       = refl
 take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
 
-drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
-           drop m (take (suc m) xs) ≡ [ lookup xs i ]
+drop-take-suc : (xs : List A) (o : Fin (length xs)) → let m = toℕ o in
+           drop m (take (suc m) xs) ≡ [ lookup xs o ]
 drop-take-suc (x ∷ xs) zero    = refl
-drop-take-suc (x ∷ xs) (suc i) = drop-take-suc xs i
+drop-take-suc (x ∷ xs) (suc o) = drop-take-suc xs o
 
-drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
-                  drop m (take (suc m) (tabulate f)) ≡ [ f i ]
-drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
-  = drop-take-suc (tabulate f) (cast _ i)
+drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (o : Fin n) → let m = toℕ o in
+                  drop m (take (suc m) (tabulate f)) ≡ [ f o ]
+drop-take-suc-tabulate f o rewrite sym (toℕ-cast (sym (length-tabulate f)) o) | sym (lookup-tabulate f o)
+  = drop-take-suc (tabulate f) (cast _ o)
 
 ------------------------------------------------------------------------
 -- splitAt

From 551515a7fd0af73dc3c37241539d451cdbdd3091 Mon Sep 17 00:00:00 2001
From: Sofia-Insa <sofia.el_boufi--crouzet@insa-rouen.fr>
Date: Tue, 27 Jun 2023 11:28:25 -0400
Subject: [PATCH 9/9] change syntaxe for Fin element from o to i

---
 src/Data/List/Properties.agda | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index b8b4a60aa0..e72fc0ca3f 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -759,15 +759,15 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
-take-suc : (xs : List A) (o : Fin (length xs)) → let m = toℕ o in
-           take (suc m) xs ≡ take m xs ∷ʳ lookup xs o
+take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
+           take (suc m) xs ≡ take m xs ∷ʳ lookup xs i
 take-suc (x ∷ xs) zero    = refl
-take-suc (x ∷ xs) (suc o) = cong (x ∷_) (take-suc xs o)
+take-suc (x ∷ xs) (suc i) = cong (x ∷_) (take-suc xs i)
 
-take-suc-tabulate : ∀ {n} (f : Fin n → A) (o : Fin n) → let m = toℕ o in
-                    take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f o
-take-suc-tabulate f o rewrite sym (toℕ-cast (sym (length-tabulate f)) o) | sym (lookup-tabulate f o)
-  = take-suc (tabulate f) (cast _ o)
+take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
+                    take (suc m) (tabulate f) ≡ take m (tabulate f) ∷ʳ f i
+take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
+  = take-suc (tabulate f) (cast _ i)
 ------------------------------------------------------------------------
 -- drop
 
@@ -781,15 +781,15 @@ take++drop zero    xs       = refl
 take++drop (suc n) []       = refl
 take++drop (suc n) (x ∷ xs) = cong (x ∷_) (take++drop n xs)
 
-drop-take-suc : (xs : List A) (o : Fin (length xs)) → let m = toℕ o in
-           drop m (take (suc m) xs) ≡ [ lookup xs o ]
+drop-take-suc : (xs : List A) (i : Fin (length xs)) → let m = toℕ i in
+           drop m (take (suc m) xs) ≡ [ lookup xs i ]
 drop-take-suc (x ∷ xs) zero    = refl
-drop-take-suc (x ∷ xs) (suc o) = drop-take-suc xs o
+drop-take-suc (x ∷ xs) (suc i) = drop-take-suc xs i
 
-drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (o : Fin n) → let m = toℕ o in
-                  drop m (take (suc m) (tabulate f)) ≡ [ f o ]
-drop-take-suc-tabulate f o rewrite sym (toℕ-cast (sym (length-tabulate f)) o) | sym (lookup-tabulate f o)
-  = drop-take-suc (tabulate f) (cast _ o)
+drop-take-suc-tabulate : ∀ {n} (f : Fin n → A) (i : Fin n) → let m = toℕ i in
+                  drop m (take (suc m) (tabulate f)) ≡ [ f i ]
+drop-take-suc-tabulate f i rewrite sym (toℕ-cast (sym (length-tabulate f)) i) | sym (lookup-tabulate f i)
+  = drop-take-suc (tabulate f) (cast _ i)
 
 ------------------------------------------------------------------------
 -- splitAt