diff --git a/CHANGELOG.md b/CHANGELOG.md
index 469c926af8..e7d776393a 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -273,6 +273,7 @@ Additions to existing modules
 
 * In `Data.List.Properties`:
   ```agda
+  length-catMaybes      : length (catMaybes xs) ≤ length xs
   applyUpTo-∷ʳ          : applyUpTo f n ∷ʳ f n ≡ applyUpTo f (suc n)
   applyDownFrom-∷ʳ      : applyDownFrom (f ∘ suc) n ∷ʳ f 0 ≡ applyDownFrom f (suc n)
   upTo-∷ʳ               : upTo n ∷ʳ n ≡ upTo (suc n)
diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda
index 8b988c646d..03e5d4ae9a 100644
--- a/src/Data/List/Base.agda
+++ b/src/Data/List/Base.agda
@@ -49,15 +49,6 @@ map : (A → B) → List A → List B
 map f []       = []
 map f (x ∷ xs) = f x ∷ map f xs
 
-mapMaybe : (A → Maybe B) → List A → List B
-mapMaybe p []       = []
-mapMaybe p (x ∷ xs) with p x
-... | just y  = y ∷ mapMaybe p xs
-... | nothing = mapMaybe p xs
-
-catMaybes : List (Maybe A) → List A
-catMaybes = mapMaybe id
-
 infixr 5 _++_
 
 _++_ : List A → List A → List A
@@ -123,11 +114,11 @@ partitionSums : List (A ⊎ B) → List A × List B
 partitionSums = partitionSumsWith id
 
 merge : {R : Rel A ℓ} → B.Decidable R → List A → List A → List A
-merge R? []       ys       = ys
-merge R? xs       []       = xs
-merge R? (x ∷ xs) (y ∷ ys) = if does (R? x y)
-  then x ∷ merge R? xs (y ∷ ys)
-  else y ∷ merge R? (x ∷ xs) ys
+merge R? []           ys           = ys
+merge R? xs           []           = xs
+merge R? x∷xs@(x ∷ xs) y∷ys@(y ∷ ys) = if does (R? x y)
+  then x ∷ merge R? xs   y∷ys
+  else y ∷ merge R? x∷xs ys
 
 ------------------------------------------------------------------------
 -- Operations for reducing lists
@@ -149,6 +140,12 @@ concatMap f = concat ∘ map f
 ap : List (A → B) → List A → List B
 ap fs as = concatMap (flip map as) fs
 
+catMaybes : List (Maybe A) → List A
+catMaybes = foldr (maybe′ _∷_ id) []
+
+mapMaybe : (A → Maybe B) → List A → List B
+mapMaybe p = catMaybes ∘ map p
+
 null : List A → Bool
 null []       = true
 null (x ∷ xs) = false
diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda
index 2d3c9e20e0..1dcf0d1a20 100644
--- a/src/Data/List/Properties.agda
+++ b/src/Data/List/Properties.agda
@@ -21,7 +21,7 @@ open import Data.List.Base as List
 open import Data.List.Membership.Propositional using (_∈_)
 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 as Maybe using (Maybe; just; nothing)
+open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe)
 open import Data.Nat.Base
 open import Data.Nat.Divisibility using (_∣_; divides; ∣n⇒∣m*n)
 open import Data.Nat.Properties
@@ -56,23 +56,23 @@ private
     C : Set c
     D : Set d
     E : Set e
+    x y z w : A
+    xs ys zs ws : List A
 
 ------------------------------------------------------------------------
 -- _∷_
 
-module _ {x y : A} {xs ys : List A} where
+∷-injective : x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys
+∷-injective refl = refl , refl
 
-  ∷-injective : x ∷ xs ≡ y List.∷ ys → x ≡ y × xs ≡ ys
-  ∷-injective refl = (refl , refl)
+∷-injectiveˡ : x ∷ xs ≡ y List.∷ ys → x ≡ y
+∷-injectiveˡ refl = refl
 
-  ∷-injectiveˡ : x ∷ xs ≡ y List.∷ ys → x ≡ y
-  ∷-injectiveˡ refl = refl
+∷-injectiveʳ : x ∷ xs ≡ y List.∷ ys → xs ≡ ys
+∷-injectiveʳ refl = refl
 
-  ∷-injectiveʳ : x ∷ xs ≡ y List.∷ ys → xs ≡ ys
-  ∷-injectiveʳ refl = refl
-
-  ∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x List.∷ xs ≡ y ∷ ys)
-  ∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)
+∷-dec : Dec (x ≡ y) → Dec (xs ≡ ys) → Dec (x ∷ xs ≡ y List.∷ ys)
+∷-dec x≟y xs≟ys = Decidable.map′ (uncurry (cong₂ _∷_)) ∷-injective (x≟y ×-dec xs≟ys)
 
 ≡-dec : DecidableEquality A → DecidableEquality (List A)
 ≡-dec _≟_ []       []       = yes refl
@@ -122,28 +122,34 @@ map-injective finj {x ∷ xs} {y ∷ ys} eq =
 ------------------------------------------------------------------------
 -- mapMaybe
 
+length-catMaybes : ∀ xs → length (catMaybes {A = A} xs) ≤ length xs
+length-catMaybes []        = ≤-refl
+length-catMaybes (just x ∷ xs) = s≤s (length-catMaybes xs)
+length-catMaybes (nothing ∷ xs) = m≤n⇒m≤1+n (length-catMaybes xs)
+
 mapMaybe-just : (xs : List A) → mapMaybe just xs ≡ xs
 mapMaybe-just []       = refl
 mapMaybe-just (x ∷ xs) = cong (x ∷_) (mapMaybe-just xs)
 
 mapMaybe-nothing : (xs : List A) →
-                   mapMaybe {B = A} (λ _ → nothing) xs ≡ []
+                   mapMaybe {B = B} (λ _ → nothing) xs ≡ []
 mapMaybe-nothing []       = refl
 mapMaybe-nothing (x ∷ xs) = mapMaybe-nothing xs
 
 module _ (f : A → Maybe B) where
 
   mapMaybe-concatMap : mapMaybe f ≗ concatMap (fromMaybe ∘ f)
-  mapMaybe-concatMap [] = refl
+  mapMaybe-concatMap []       = refl
   mapMaybe-concatMap (x ∷ xs) with ih ← mapMaybe-concatMap xs | f x
   ... | just y  = cong (y ∷_) ih
   ... | nothing = ih
 
   length-mapMaybe : ∀ xs → length (mapMaybe f xs) ≤ length xs
-  length-mapMaybe []       = z≤n
-  length-mapMaybe (x ∷ xs) with ih ← length-mapMaybe xs | f x
-  ... | just y  = s≤s ih
-  ... | nothing = m≤n⇒m≤1+n ih
+  length-mapMaybe xs = ≤-begin
+    length (mapMaybe f xs)      ≤⟨ length-catMaybes (map f xs) ⟩
+    length (map f xs)           ≤⟨ ≤-reflexive (length-map f xs) ⟩
+    length xs                   ≤-∎
+    where open ≤-Reasoning renaming (begin_ to ≤-begin_; _∎ to _≤-∎)
 
 ------------------------------------------------------------------------
 -- _++_
@@ -175,14 +181,14 @@ module _ {A : Set a} where
   ++-identityʳ-unique : ∀ (xs : List A) {ys} → xs ≡ xs ++ ys → ys ≡ []
   ++-identityʳ-unique []       refl = refl
   ++-identityʳ-unique (x ∷ xs) eq   =
-    ++-identityʳ-unique xs (proj₂ (∷-injective eq))
+    ++-identityʳ-unique xs (∷-injectiveʳ eq)
 
   ++-identityˡ-unique : ∀ {xs} (ys : List A) → xs ≡ ys ++ xs → ys ≡ []
   ++-identityˡ-unique               []       _  = refl
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ ys) eq
     with ++-identityˡ-unique (ys ++ [ x ]) (begin
-         xs                  ≡⟨ proj₂ (∷-injective eq) ⟩
-         ys ++ x ∷ xs        ≡⟨ sym (++-assoc ys [ x ] xs) ⟩
+         xs                  ≡⟨ ∷-injectiveʳ eq ⟩
+         ys ++ x ∷ xs        ≡⟨ ++-assoc ys [ x ] xs ⟨
          (ys ++ [ x ]) ++ xs ∎)
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ []   ) eq | ()
   ++-identityˡ-unique {xs = x ∷ xs} (y ∷ _ ∷ _) eq | ()
@@ -1215,22 +1221,20 @@ reverse-downFrom = reverse-applyDownFrom id
 ------------------------------------------------------------------------
 -- _∷ʳ_
 
-module _ {x y : A} where
-
-  ∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
-  ∷ʳ-injective []          []          refl = (refl , refl)
-  ∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with refl , eq′  ← ∷-injective eq
-    = Product.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′)
-  ∷ʳ-injective []          (_ ∷ _ ∷ _) ()
-  ∷ʳ-injective (_ ∷ _ ∷ _) []          ()
+∷ʳ-injective : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys × x ≡ y
+∷ʳ-injective []          []          refl = refl , refl
+∷ʳ-injective (x ∷ xs)    (y  ∷ ys)   eq   with refl , eq′  ← ∷-injective eq
+  = Product.map (cong (x ∷_)) id (∷ʳ-injective xs ys eq′)
+∷ʳ-injective []          (_ ∷ _ ∷ _) ()
+∷ʳ-injective (_ ∷ _ ∷ _) []          ()
 
-  ∷ʳ-injectiveˡ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
-  ∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq)
+∷ʳ-injectiveˡ : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → xs ≡ ys
+∷ʳ-injectiveˡ xs ys eq = proj₁ (∷ʳ-injective xs ys eq)
 
-  ∷ʳ-injectiveʳ : ∀ (xs ys : List A) → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
-  ∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)
+∷ʳ-injectiveʳ : ∀ xs ys → xs ∷ʳ x ≡ ys ∷ʳ y → x ≡ y
+∷ʳ-injectiveʳ xs ys eq = proj₂ (∷ʳ-injective xs ys eq)
 
-∷ʳ-++ : ∀ (xs : List A) (a : A) (ys : List A) → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
+∷ʳ-++ : ∀ xs (a : A) ys → xs ∷ʳ a ++ ys ≡ xs ++ a ∷ ys
 ∷ʳ-++ xs a ys = ++-assoc xs [ a ] ys