diff --git a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean
index acff1fcd0..3f7ba3903 100644
--- a/Cslib/Foundations/Data/OmegaSequence/Flatten.lean
+++ b/Cslib/Foundations/Data/OmegaSequence/Flatten.lean
@@ -150,7 +150,7 @@ theorem flatten_drop [Inhabited α]
   (flatten_take_drop h_ls n).2
 
 /-- `ls n` is the segement from position `ls.cumLen n` to position `ls.cumLen (n + 1) - 1`
-of ls.flatten` -/
+of `ls.flatten` -/
 @[simp, scoped grind =]
 theorem extract_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0)
     (n : ℕ) : ls.flatten.extract (ls.cumLen n) (ls.cumLen (n + 1)) = ls n := by
@@ -159,6 +159,15 @@ theorem extract_flatten [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k
   have h_take := flatten_take h_ls' 1
   grind [extract_eq_drop_take]
 
+/-- Distributivity of "forall" over `flatten`. -/
+theorem forall_flatten_iff [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ k, (ls k).length > 0)
+    (p : α → Prop) : (∀ n, p (ls.flatten n)) ↔ ∀ k, (ls k).Forall p := by
+  constructor
+  · simp only [List.forall_iff_forall_mem, List.forall_mem_iff_getElem, ← extract_flatten h_ls]
+    grind
+  · have := segment_upper_bound (cumLen_strictMono h_ls)
+    grind [List.forall_iff_forall_mem, flatten_def]
+
 /-- Given an ω-sequence `s` and a function `f : ℕ → ℕ`, `s.toSegs f` is the ω-sequence
 whose `n`-th element is the list `s.extract (f n) (f (n + 1))`.  In all its uses, the
 function `f` will always be assumed to be strictly monotonic with `f 0 = 0`. -/