diff --git a/Utils.agda b/Utils.agda
index 9156f3b..21e1b47 100644
--- a/Utils.agda
+++ b/Utils.agda
@@ -32,6 +32,10 @@ All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x
 All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
 All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
 
+All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
+All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
+All-single {c = c} {l = x ∷ xs} (p ∷ ps) (there c∈xs) = All-single ps c∈xs
+
 All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs
 All-x∈xs [] = []
 All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')