diff --git a/CHANGELOG.md b/CHANGELOG.md
index ebaed12a67..9874c5593d 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -313,6 +313,12 @@ Additions to existing modules
                deduplicate _≟_ (xs ++ ys) ↭ deduplicate _≟_ xs ++ deduplicate _≟_ ys
   ```
 
+* In `Data.List.Relation.Unary.First.Properties`:
+  ```agda
+  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
+  ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
+  ```
+
 * In `Data.Maybe.Properties`:
   ```agda
   maybe′-∘ : ∀ f g → f ∘ (maybe′ g b) ≗ maybe′ (f ∘ g) (f b)
@@ -417,9 +423,3 @@ Additions to existing modules
   does-≐ : P ≐ Q → (P? : Decidable P) → (Q? : Decidable Q) → does ∘ P? ≗ does ∘ Q?
   does-≡ : (P? P?′ : Decidable P) → does ∘ P? ≗ does ∘ P?′
   ```
-
-* In `Data.List.Relation.Unary.First.Properties`:
-  ```agda
-  ¬First⇒All : ∁ Q ⊆ P → ∁ (First P Q) ⊆ All P
-  ```
-
diff --git a/src/Data/List/Relation/Unary/First/Properties.agda b/src/Data/List/Relation/Unary/First/Properties.agda
index b83d85d8d8..dac49597b1 100644
--- a/src/Data/List/Relation/Unary/First/Properties.agda
+++ b/src/Data/List/Relation/Unary/First/Properties.agda
@@ -8,6 +8,7 @@
 
 module Data.List.Relation.Unary.First.Properties where
 
+open import Data.Bool.Base using (true; false)
 open import Data.Fin.Base using (suc)
 open import Data.List.Base as List using (List; []; _∷_)
 open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
@@ -16,8 +17,9 @@ open import Data.List.Relation.Unary.First
 import Data.Sum.Base as Sum
 open import Function.Base using (_∘′_; _∘_; id)
 open import Relation.Binary.PropositionalEquality.Core as ≡ using (_≡_; refl; _≗_)
-import Relation.Nullary.Decidable.Core as Dec
+open import Relation.Nullary.Decidable.Core as Dec
 open import Relation.Nullary.Negation.Core using (contradiction)
+open import Relation.Nullary.Reflects using (invert)
 open import Relation.Unary using (Pred; _⊆_; ∁; Irrelevant; Decidable)
 
 ------------------------------------------------------------------------
@@ -65,6 +67,13 @@ module _ {a p q} {A : Set a} {P : Pred A p} {Q : Pred A q} where
     let px = ¬q⇒p (¬pqxxs ∘ [_]) in
     px ∷ ¬First⇒All ¬q⇒p (¬pqxxs ∘ (px ∷_))
 
+  ¬All⇒First : Decidable P → ∁ P ⊆ Q → ∁ (All P) ⊆ First P Q
+  ¬All⇒First P? ¬p⇒q {x = []} ¬⊤ = contradiction [] ¬⊤
+  ¬All⇒First P? ¬p⇒q {x = x ∷ xs} ¬∀ with P? x
+  ... |  true because  [px] = let px = invert [px] in
+                              px ∷ ¬All⇒First P? ¬p⇒q (¬∀ ∘ (px ∷_))
+  ... | false because [¬px] = [ ¬p⇒q (invert [¬px]) ]
+
 ------------------------------------------------------------------------
 -- Irrelevance