Computation.exists_of_mem_parallel

theorem Computation.exists_of_mem_parallel : ∀ {α : Type u} {S : Stream'.WSeq (Computation α)} {a : α}, a ∈ Computation.parallel S → ∃ c ∈ S, a ∈ c

This theorem states that for any type `α`, any infinite stream `S` of computations of type `α`, and any value `a` of type `α`, if `a` is in the result of the parallel computation of `S`, then there exists a computation `c` in `S` such that `a` is in `c`. In other words, if a value is produced by running multiple computations in parallel, then there must be at least one individual computation that produces that value.

More concisely: For any type `α`, infinite stream `S` of computations of type `α`, and value `a` of type `α`, if `a` is in the result of the parallel computation of `S`, then there exists some computation `c` in `S` such that `a` is in the result of `c`.