diff --git a/CHANGELOG.md b/CHANGELOG.md
index 628862540d..28aa64402f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -2082,7 +2082,8 @@ 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-all : n ≥ length xs → take n xs ≡ xs     
   take-[] : ∀ m → take  m [] ≡ []
   drop-[] : ∀ m → drop  m [] ≡ []
   ```
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 58d5b39680..feb17351d5 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -758,6 +758,12 @@ length-take zero    xs       = refl
 length-take (suc n) []       = refl
 length-take (suc n) (x ∷ xs) = cong suc (length-take n xs)
 
+-- If you take at least as many elements from a list as it has, you get the whole list.
+take-all :(n : ℕ) (xs : List A) → n ≥ length xs → take n xs ≡ xs
+take-all zero [] _ = refl
+take-all (suc _) [] _ = refl
+take-all (suc n) (x ∷ xs) (s≤s pf) = cong (x ∷_) (take-all n xs pf)
+
 -- Taking from an empty list does nothing.
 take-[] : ∀ m → take {A = A} m [] ≡ []
 take-[] zero = refl