diff --git a/CHANGELOG.md b/CHANGELOG.md
index b1b77d98f5..c94f305170 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -101,6 +101,9 @@ New modules
 * `Codata.Guarded.Stream.Relation.Unary.Linked` for a proof that each pair
   of consecutive elements of a stream are related.
 
+* `Data.Bool.ListAction.Properties` for properties of conjunction and
+  disjunction of lists.
+
 * A new type of lists that grow on the right.
   This is typically useful to model contexts of typing rules
   or type accumulators that need to be reversed in the base case.
diff --git a/src/Data/Bool/ListAction/Properties.agda b/src/Data/Bool/ListAction/Properties.agda
new file mode 100644
index 0000000000..7fd34e8260
--- /dev/null
+++ b/src/Data/Bool/ListAction/Properties.agda
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Booleans: properties of conjunction and disjunction of lists
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Bool.ListAction.Properties where
+
+open import Data.Bool.Base
+open import Data.Bool.Properties
+open import Data.Bool.ListAction
+open import Data.List.Base hiding (and; or; all; any)
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Binary.Permutation.Propositional using (_↭_; ↭⇒↭ₛ)
+import Data.List.Relation.Binary.Permutation.Propositional.Properties as ↭
+open import Data.List.Relation.Binary.Permutation.Setoid.Properties
+open import Data.List.Relation.Unary.Any using (here; there)
+open import Function.Base using (_∘′_)
+open import Relation.Binary.Core using (_Preserves_⟶_)
+open import Relation.Binary.PropositionalEquality.Core
+open import Relation.Binary.PropositionalEquality.Properties
+  using (module ≡-Reasoning)
+
+------------------------------------------------------------------------
+-- Properties
+
+-- and
+
+and-++ : ∀ bs cs → and (bs ++ cs) ≡ and bs ∧ and cs
+and-++ [] cs = refl
+and-++ (b ∷ bs) cs = begin
+  b ∧ and (bs ++ cs)    ≡⟨ cong (b ∧_) (and-++ bs cs) ⟩
+  b ∧ (and bs ∧ and cs) ≡⟨ ∧-assoc b (and bs) (and cs) ⟨
+  (b ∧ and bs) ∧ and cs ∎
+  where open ≡-Reasoning
+
+∨-distribˡ-and : ∀ b cs → b ∨ and cs ≡ all (b ∨_) cs
+∨-distribˡ-and b [] = ∨-zeroʳ b
+∨-distribˡ-and b (c ∷ cs) = trans (∨-distribˡ-∧ b c (and cs)) (cong ((b ∨ c) ∧_) (∨-distribˡ-and b cs))
+
+∨-distribʳ-and : ∀ b cs → and cs ∨ b ≡ all (_∨ b) cs
+∨-distribʳ-and b [] = ∨-zeroˡ b
+∨-distribʳ-and b (c ∷ cs) = trans (∨-distribʳ-∧ b c (and cs)) (cong ((c ∨ b) ∧_) (∨-distribʳ-and b cs))
+
+and-↭ : and Preserves _↭_ ⟶ _≡_
+and-↭ p = foldr-commMonoid ≡-setoid ∧-isCommutativeMonoid (↭⇒↭ₛ p)
+
+and-locate : ∀ bs → and bs ≡ false → false ∈ bs
+and-locate (false ∷ bs) p = here refl
+and-locate (true ∷ bs) p = there (and-locate bs p)
+
+-- or
+
+or-++ : ∀ bs cs → or (bs ++ cs) ≡ or bs ∨ or cs
+or-++ [] cs = refl
+or-++ (b ∷ bs) cs = begin
+  b ∨ or (bs ++ cs)   ≡⟨ cong (b ∨_) (or-++ bs cs) ⟩
+  b ∨ (or bs ∨ or cs) ≡⟨ ∨-assoc b (or bs) (or cs) ⟨
+  (b ∨ or bs) ∨ or cs ∎
+  where open ≡-Reasoning
+
+∧-distribˡ-or : ∀ b cs → b ∧ or cs ≡ any (b ∧_) cs
+∧-distribˡ-or b [] = ∧-zeroʳ b
+∧-distribˡ-or b (c ∷ cs) = trans (∧-distribˡ-∨ b c (or cs)) (cong ((b ∧ c) ∨_) (∧-distribˡ-or b cs))
+
+∧-distribʳ-or : ∀ b cs → or cs ∧ b ≡ any (_∧ b) cs
+∧-distribʳ-or b [] = ∧-zeroˡ b
+∧-distribʳ-or b (c ∷ cs) = trans (∧-distribʳ-∨ b c (or cs)) (cong ((c ∧ b) ∨_) (∧-distribʳ-or b cs))
+
+or-↭ : or Preserves _↭_ ⟶ _≡_
+or-↭ p = foldr-commMonoid ≡-setoid ∨-isCommutativeMonoid (↭⇒↭ₛ p)
+
+or-locate : ∀ bs → or bs ≡ true → true ∈ bs
+or-locate (false ∷ bs) p = there (or-locate bs p)
+or-locate (true ∷ bs) p = here p
+
+-- all
+
+all-↭ : ∀ {a} {A : Set a} (p : A → Bool) → all p Preserves _↭_ ⟶ _≡_
+all-↭ p = and-↭ ∘′ ↭.map⁺ p
+
+-- any
+
+any-↭ : ∀ {a} {A : Set a} (p : A → Bool) → any p Preserves _↭_ ⟶ _≡_
+any-↭ p = or-↭ ∘′ ↭.map⁺ p